Closed shym closed 1 year ago
Add a pre-push dune alias to check that all the files appearing in dune.incs are indeed tracked in git, to (help) avoid pushing dune.incs generated for local-only files.
pre-push
dune.inc
git
This is brittle and incomplete (see #328 for something it would have missed).
Add a
pre-push
dune alias to check that all the files appearing indune.inc
s are indeed tracked ingit
, to (help) avoid pushingdune.inc
s generated for local-only files.