diff options
| author | Pierre-Marie Pédrot | 2015-03-04 16:22:24 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-03-04 16:22:24 +0100 |
| commit | a348471ec6303b9b080d77cf0ca7a58c21aa6369 (patch) | |
| tree | 0746249e326b92fb21f98fe71e467f0ee0215058 /tools | |
| parent | d169ecbac96fe2a8a6a44395ad7fa83612e725c4 (diff) | |
| parent | 00018101cf81f69d23587985a16fe3c8eefb8eaf (diff) | |
Merge branch 'v8.5'
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/coq_makefile.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index 93df848de4..1e0bfacf93 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -330,6 +330,7 @@ let clean sds sps = if !some_vfile then begin print "\trm -f $(OBJFILES) $(OBJFILES:.o=.native) $(NATIVEFILES)\n"; + print "\tfind . -name .coq-native -type d -empty -delete\n"; print "\trm -f $(VOFILES) $(VOFILES:.vo=.vio) $(GFILES) $(VFILES:.v=.v.d) $(VFILES:=.beautified) $(VFILES:=.old)\n" end; print "\trm -f all.ps all-gal.ps all.pdf all-gal.pdf all.glob $(VFILES:.v=.glob) $(VFILES:.v=.tex) $(VFILES:.v=.g.tex) all-mli.tex\n"; @@ -366,7 +367,7 @@ let implicit () = print "$(filter-out $(addsuffix .cmx,$(foreach lib,$(MLPACKFILES:.mlpack=_MLPACK_DEPENDENCIES),$($(lib)))),$(ML4FILES:.ml4=.cmx)): %.cmx: %.ml4\n"; print "\t$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) $(PP) -impl $<\n\n"; print "$(addsuffix .d,$(ML4FILES)): %.ml4.d: %.ml4\n"; - print "\t$(COQDEP) $(OCAMLLIBS) \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n" in + print "\t$(OCAMLDEP) -slash $(OCAMLLIBS) $(PP) -impl \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n" in let ml_rules () = print "$(MLFILES:.ml=.cmo): %.cmo: %.ml\n\t$(CAMLC) $(ZDEBUG) $(ZFLAGS) $<\n\n"; print "$(filter-out $(addsuffix .cmx,$(foreach lib,$(MLPACKFILES:.mlpack=_MLPACK_DEPENDENCIES),$($(lib)))),$(MLFILES:.ml=.cmx)): %.cmx: %.ml\n"; |