[duneproject][Bugfix] Make sure dune_enable_all_packages() can actually be disabled
The shell script logic for switching dune_enable_all_packages() on or off in duneproject was broken and always turned the feature on, ignoring the user input. Fixed by testing for the actual contents of the variable instead of its length and by converting the contents to lowercase before. (cherry picked from commit 346657b7) Signed-off-by:Carsten Gräser <graeser@dune-project.org>
Please register or sign in to comment