diff options
| author | Enrico Tassi | 2018-09-11 11:02:18 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2018-09-11 11:02:18 +0200 |
| commit | 3dceb51345662b4ceda4214be5ae2d17459f48f3 (patch) | |
| tree | 4166d259173004a4fc3dd453e6a59a4ad6febfbb | |
| parent | 356a421695706e14781d581d1908e07bdd3f237a (diff) | |
| parent | b27383a71ac10140e0b5b76426cdd74225f33f64 (diff) | |
Merge PR #8452: Fix #8358: circular make dependency for camldevfiles
| -rw-r--r-- | Makefile | 3 |
1 files changed, 3 insertions, 0 deletions
@@ -177,6 +177,9 @@ Makefile $(wildcard Makefile.*) config/Makefile : ; ########################################################################### camldevfiles: $(MERLINFILES) META.coq +# prevent submake dependency +META.coq.in $(MERLININFILES): ; + .merlin: .merlin.in cp -a "$<" "$@" |