diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-05-01 19:31:45 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-05-01 19:32:59 +0200 |
| commit | 3ce7ae5c2de955d5d79fc23a02ee06fa9071f24a (patch) | |
| tree | 71c1fe2f993c311b4f1df6b6f0b6e128548581d5 /tools/coq_makefile.ml | |
| parent | 97ee8fbd0bf917c29e47f746c0a28623ebc7da9a (diff) | |
Automatically run alienclean before compiling.
This removes the "leftover files without known source" error in favor
of automatic handling.
Diffstat (limited to 'tools/coq_makefile.ml')
0 files changed, 0 insertions, 0 deletions