Skip to content
Snippets Groups Projects

dunemodules.lib: skip directories starting with dot when looking for modules

Merged dunemodules.lib: skip directories starting with dot when looking for modules
ansgar/dune-common:dunemodules-skip-directories-with-dot into master
All threads resolved!
Merged Ansgar Burchardt requested to merge ansgar/dune-common:dunemodules-skip-directories-with-dot into master
All threads resolved!
Compare
and
1 file
+ 1
− 1
Compare changes
  • Side-by-side
  • Inline
lib/dunemodules.lib
+ 1
− 1
@@ -274,7 +274,7 @@ find_modules_in_path() {
while read m; do
test -n "$m" && parse_control "$m"
done <<EOFM
$(find -H "$dir" -name $CONTROL | $GREP -v 'dune-[-_a-zA-Z]/dune-[-a-zA-Z_]*-[0-9]\{1,\}.[0-9]\{1,\}/')
$(find -H "$dir" -type d -name .git -prune -o -name $CONTROL -print | $GREP -v 'dune-[-_a-zA-Z]/dune-[-a-zA-Z_]*-[0-9]\{1,\}.[0-9]\{1,\}/')
EOFM
else
parse_control "$dir"