diff options
| author | Pierre Boutillier | 2015-01-13 23:26:13 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2015-01-15 06:56:11 +0100 |
| commit | 8f077f6d05d0c764e401ce6770f6b598523c33fc (patch) | |
| tree | 569e849ed018a77f36eeec81ef54f6b9708ce50e /tools | |
| parent | fa397ec05fdfea053470cddafd1ab09a710f5bc9 (diff) | |
coq_makefile installs native files
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/coq_makefile.ml | 11 |
1 files changed, 5 insertions, 6 deletions
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index ac3f6fc8b3..d877ed564a 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -257,7 +257,7 @@ let install (vfiles,(mlifiles,ml4files,mlfiles,mllibfiles,mlpackfiles),_,sds) in let cmxsfiles = List.rev_append cmofiles mllibfiles in let where_what_cmxs = vars_to_put_by_root [("CMXSFILES",cmxsfiles)] inc in let where_what_oth = vars_to_put_by_root - [("VOFILES",vfiles);("CMOFILES",cmofiles);("CMIFILES",cmifiles);("CMAFILES",mllibfiles)] + [("VOFILES",vfiles);("NATIVEFILES",vfiles);("CMOFILES",cmofiles);("CMIFILES",cmifiles);("CMAFILES",mllibfiles)] inc in let doc_dir = where_put_doc inc in let () = if is_install = Project_file.UnspecInstall then @@ -328,9 +328,7 @@ let clean sds sps = end; if !some_vfile then begin - print "\trm -f $(OBJFILES) $(OBJFILES:.o=.native)\n"; - print "\trm -f $(OBJFILES:.o=.cmi) $(OBJFILES:.o=.cmo)\n"; - print "\trm -f $(OBJFILES:.o=.cmx) $(OBJFILES:.o=.cmxs)\n"; + print "\trm -f $(OBJFILES) $(OBJFILES:.o=.native) $(NATIVEFILES)\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"; @@ -577,8 +575,9 @@ let main_targets vfiles (mlifiles,ml4files,mlfiles,mllibfiles,mlpackfiles) other print "GFILES:=$(VFILES:.v=.g)\n"; print "HTMLFILES:=$(VFILES:.v=.html)\n"; print "GHTMLFILES:=$(VFILES:.v=.g.html)\n"; - print "OBJFILES:=$(call vo_to_obj,$(VOFILES))\n"; - classify_files_by_root "OBJFILES" l inc + print "OBJFILES=$(call vo_to_obj,$(VOFILES))\n"; + print "NATIVEFILES=$(OBJFILES:.o=.cmi) $(OBJFILES:.o=.cmo) $(OBJFILES:.o=.cmx) $(OBJFILES:.o=.cmxs)\n"; + classify_files_by_root "NATIVEFILES" l inc end; decl_var "ML4FILES" ml4files; decl_var "MLFILES" mlfiles; |