diff options
| author | Gaëtan Gilbert | 2018-09-10 18:34:57 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-09-10 18:34:57 +0200 |
| commit | b27383a71ac10140e0b5b76426cdd74225f33f64 (patch) | |
| tree | a72f6c640bfb4c64dda5eb5053689bc380873805 | |
| parent | 087588553d31752fadbb65ade9d377176412f316 (diff) | |
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 "$<" "$@" |