projects / dune-common.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 3751494) | patch
skip directories starting with a dot when looking for dune.module
authorAnsgar Burchardt <ansgar@debian.org>
Thu, 12 Jan 2023 15:39:41 +0000 (15:39 +0000)
committerMarkus Blatt <markus@dr-blatt.de>
Thu, 12 Jan 2023 15:39:41 +0000 (15:39 +0000)
commit8e2bb62f6cdeeb04678e66a3707fc811653659b2
tree4ddb25b3cf8241b64eaca750387c63487a07fd3btree | snapshot
parent375149422e2e48688cfa49de8a5c1072ecd75d6acommit | 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.