dunemodules.lib: skip directories starting with dot when looking for modules (!1184) · Merge requests · Core Modules / dune-common · GitLab

Ansgar Burchardt requested to merge ansgar/dune-common:dunemodules-skip-directories-with-dot into master Oct 20, 2022

Reference: https://lists.dune-project.org/pipermail/dune-devel/2022-October/002961.html

Closes #320 (closed)

Edited Oct 24, 2022 by Simon Praetorius