projects / dune-common.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 2029cdb) | patch
skip directories starting with a dot when looking for dune.module
authorAnsgar Burchardt <ansgar@debian.org>
Tue, 26 Dec 2023 18:41:53 +0000 (19:41 +0100)
committerAnsgar <ansgar@debian.org>
Tue, 26 Dec 2023 18:41:53 +0000 (19:41 +0100)
commit225b82d4e7b10905a3b99d566b90d230b0eaf977
tree0153c121111d5134dcce91bb21212b160d201af5tree | snapshot
parent2029cdbf1c4b2724a6feb82e23af8aa9d9f0b3f4commit | 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.