projects / dune-common.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 993d1a3) | patch
skip directories starting with a dot when looking for dune.module
authorAnsgar Burchardt <ansgar@debian.org>
Sat, 19 Mar 2022 12:10:34 +0000 (12:10 +0000)
committerDrew Parsons <dparsons@debian.org>
Sat, 19 Mar 2022 12:10:34 +0000 (12:10 +0000)
commit8efe447dc458f5f53dee8c26a1b34bfdfe14da19
tree569b937884ba8068698fe9817b2d0e3d491109fftree | snapshot
parent993d1a3a1459fe6535a8cd6c48509e61deeea7b6commit | diff
skip directories starting with a dot when looking for dune.module

===================================================================

Gbp-Pq: Name skip-dirs-starting-with-dot.patch
lib/dunemodules.lib diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.