diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2015-01-15 07:49:27 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2015-01-15 07:49:27 +0100 |
| commit | 530dcf1e6cd008e89a527dacb836202bcb2d02db (patch) | |
| tree | f1cef094ab0ca6070f990c45da142ef1e42dd261 /tools | |
| parent | 8f077f6d05d0c764e401ce6770f6b598523c33fc (diff) | |
Make installation of native files more robust.
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/coq_makefile.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index d877ed564..28b86ddc7 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -505,7 +505,7 @@ let parameters () = print "TIMER=$(if $(TIMED), $(STDTIME), $(TIMECMD))\n\n"; print "vo_to_obj = $(addsuffix .o,$(foreach vo,$(1),\\\n"; print " $(addprefix $(dir $(vo)),$(addprefix .coq-native/,$(filter-out Warning: Error:,$(firstword \\\n"; - print " $(shell $(COQBIN)coqtop -batch -quiet -print-mod-uid $(vo))))))))\n\n" + print " $(shell $(COQBIN)coqtop -q -noinit -batch -quiet -print-mod-uid $(vo))))))))\n\n" let include_dirs (inc_ml,inc_i,inc_r) = let parse_ml_includes l = List.map (fun (x,_) -> "-I \"" ^ x ^ "\"") l in @@ -576,7 +576,8 @@ let main_targets vfiles (mlifiles,ml4files,mlfiles,mllibfiles,mlpackfiles) other print "HTMLFILES:=$(VFILES:.v=.html)\n"; print "GHTMLFILES:=$(VFILES:.v=.g.html)\n"; print "OBJFILES=$(call vo_to_obj,$(VOFILES))\n"; - print "NATIVEFILES=$(OBJFILES:.o=.cmi) $(OBJFILES:.o=.cmo) $(OBJFILES:.o=.cmx) $(OBJFILES:.o=.cmxs)\n"; + print "ALLNATIVEFILES=$(OBJFILES:.o=.cmi) $(OBJFILES:.o=.cmo) $(OBJFILES:.o=.cmx) $(OBJFILES:.o=.cmxs)\n"; + print "NATIVEFILES=$(foreach f, $(ALLNATIVEFILES), $(wildcard $f))\n"; classify_files_by_root "NATIVEFILES" l inc end; decl_var "ML4FILES" ml4files; |