diff options
| author |  notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-06-09 15:05:37 +0000 |
|---|---|---|
| committer | notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-06-09 15:05:37 +0000 |
| commit | 6f593f5ef05f6a1a7bf4cd2ce6d59c41345e034b (patch) | |
| tree | e7ba339f5ba4ed1e7c551b0b38c88feb8ec00edf /tools | |
| parent | 9d331b4cd70e328b3398bf0d84d4e2d02d0830bf (diff) | |
Remplacement des echo -e par printf + bug sur les exécutables ocaml dans coq_makefile
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11079 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/coq_makefile.ml4 | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/tools/coq_makefile.ml4 b/tools/coq_makefile.ml4 index 2a5be13d3..a34e21fb5 100644 --- a/tools/coq_makefile.ml4 +++ b/tools/coq_makefile.ml4 @@ -108,7 +108,7 @@ let standard sds sps = print "\trm -f all.ps all-gal.ps all.glob $(VFILES:.v=.glob) $(HTMLFILES) \ $(GHTMLFILES) $(VFILES:.v=.tex) $(VFILES:.v=.g.tex) $(VFILES:.v=.v.d)\n"; if !some_mlfile then - print "\trm -f $(CMOFILES) $(MLFILES:.ml=.ml.d)\n"; + print "\trm -f $(CMOFILES) $(MLFILES:.ml=.cmi) $(MLFILES:.ml=.ml.d)\n"; print "\t- rm -rf html\n"; List.iter (fun (file,_,_) -> print "\t- rm -f "; print file; print "\n") @@ -184,8 +184,8 @@ let variables l = (* Caml executables and relative variables *) printf "CAMLC:=$(CAMLBIN)ocamlc -rectypes -c\n"; printf "CAMLOPTC:=$(CAMLBIN)ocamlopt -rectypes -c\n"; - printf "CAMLLINK:=$(CAMLBIN)ocamlc\n"; - printf "CAMLOPTLINK:=$(CAMLBIN)ocamlopt\n"; + printf "CAMLLINK:=$(CAMLBIN)ocamlc -rectypes\n"; + printf "CAMLOPTLINK:=$(CAMLBIN)ocamlopt -rectypes\n"; print "GRAMMARS:=grammar.cma\n"; print "CAMLP4EXTEND:=pa_extend.cmo pa_macro.cmo q_MLast.cmo\n"; print "PP:=-pp \"$(CAMLBIN)$(CAMLP4)o -I . -I $(COQTOP)/parsing $(CAMLP4EXTEND) $(GRAMMARS) -impl\"\n"; |