diff --git a/bin/duneproject b/bin/duneproject index fe8c6139c4188b4b89b9355cb6d0250168075573..e28e11a66feb51ad7352ad0e20e10f9d1e5bf63f 100755 --- a/bin/duneproject +++ b/bin/duneproject @@ -148,19 +148,13 @@ export PKG_CONFIG_PATH="$PKG_CONFIG_PATH:$(canonicalpath $0)/../lib/pkgconfig" # search for modules, both installed and src modules find_modules_in_path -echo "FOUND_MODULES=$FOUND_MODULES" - # get the real module names MODULES="" for i in $FOUND_MODULES; do mod=$(eval echo \$NAME_$i) - MODULES="$SRC_MODULES$mod " -echo "$i ... MODULES=$MODULES" >&2 - + MODULES="$MODULES$mod " done -echo "MODULES=$MODULES" >&2 - if [ "$MODULES" = "" ]; then echo "ERROR:">&2 echo " No dune modules were found!">&2