diff options
| author |  Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2015-05-14 16:38:21 +0200 |
|---|---|---|
| committer | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2015-05-14 16:38:21 +0200 |
| commit | 3fb81febe8efc34860688cac88a2267cfe298cf7 (patch) | |
| tree | 1b36449d1bdb7aa29be30cda15d63d36134f2a56 /tools | |
| parent | 5f8dc36fb2d65699233b9ac9a3ff9f93701a01cb (diff) | |
Do not regenerate .d files when cleaning them. (Fix bug #4079)
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/coq_makefile.ml | 9 |
1 files changed, 7 insertions, 2 deletions
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index 00088570b..8f4772e28 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -575,8 +575,13 @@ let main_targets vfiles (mlifiles,ml4files,mlfiles,mllibfiles,mlpackfiles) other let decl_var var = function |[] -> () |l -> - printf "%s:=" var; print_list "\\\n " l; print "\n"; - printf "\n-include $(addsuffix .d,$(%s))\n.SECONDARY: $(addsuffix .d,$(%s))\n\n" var var + printf "%s:=" var; print_list "\\\n " l; print "\n\n"; + print "ifneq ($(filter-out archclean clean cleanall printenv,$(MAKECMDGOALS)),)\n"; + printf "-include $(addsuffix .d,$(%s))\n" var; + print "else\nifeq ($(MAKECMDGOALS),)\n"; + printf "-include $(addsuffix .d,$(%s))\n" var; + print "endif\nendif\n\n"; + printf ".SECONDARY: $(addsuffix .d,$(%s))\n\n" var in section "Files dispatching."; decl_var "VFILES" vfiles; |