diff options
Diffstat (limited to 'tools')
-rw-r--r-- | tools/coq_makefile.ml | 9 | ||||
-rw-r--r-- | tools/coqc.ml | 4 |
2 files changed, 9 insertions, 4 deletions
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index 11b4b3732..36d29a1e8 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; diff --git a/tools/coqc.ml b/tools/coqc.ml index 7e822dbe3..aed229abc 100644 --- a/tools/coqc.ml +++ b/tools/coqc.ml @@ -109,7 +109,7 @@ let parse_args () = |"-q"|"-full"|"-profile"|"-just-parsing"|"-echo" |"-unsafe"|"-quiet" |"-silent"|"-m"|"-xml"|"-v7"|"-v8"|"-beautify"|"-strict-implicit" |"-dont-load-proofs"|"-load-proofs"|"-force-load-proofs" - |"-impredicative-set"|"-vm"|"-no-native-compiler" + |"-impredicative-set"|"-vm"|"-native-compiler" |"-verbose-compat-notations"|"-no-compat-notations" |"-indices-matter"|"-quick"|"-color"|"-type-in-type" |"-async-proofs-always-delegate"|"-async-proofs-never-reopen-branch" @@ -122,7 +122,7 @@ let parse_args () = |"-load-vernac-source"|"-l"|"-load-vernac-object" |"-load-ml-source"|"-require"|"-load-ml-object" |"-init-file"|"-dump-glob"|"-compat"|"-coqlib"|"-top" - |"-async-proofs-j" |"-async-proofs-private-flags" |"-async-proofs" + |"-async-proofs-j" |"-async-proofs-private-flags" |"-async-proofs"|"-w" as o) :: rem -> begin match rem with |