projects / dune-common.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: e737a55) | patch
skip directories starting with a dot when looking for dune.module
authorAnsgar Burchardt <ansgar@debian.org>
Wed, 15 Jul 2020 10:29:39 +0000 (11:29 +0100)
committerAnsgar <ansgar@debian.org>
Wed, 15 Jul 2020 10:29:39 +0000 (11:29 +0100)
commit120b3a381de20bdddd3ca80f40d615420b98e594
tree1ad23e99eb156170415c73130401911c1a71ba7dtree | snapshot
parente737a5525f89f368600ec926fcefc23cf41ae85ecommit | 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.