aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7>2001-05-28 12:25:38 +0000
committerGravatar filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7>2001-05-28 12:25:38 +0000
commitb7c83140ffcfef871ac2d8eab342ec489f298c8a (patch)
treec170fdbdbf365c5c02875781c7c5de6f9f1d193c
parent6dc94fe5c1e02fccefbfedfcb1d4347274f3de0b (diff)
option -byte
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1769 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r--tools/coq_makefile.ml10
1 files changed, 2 insertions, 8 deletions
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index ce220b54f..e0177396b 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -171,15 +171,9 @@ let variables l =
-I $(COQTOP)/proofs -I $(COQTOP)/syntax -I $(COQTOP)/tactics \\
-I $(COQTOP)/toplevel -I $(CAMLP4LIB)\n";
print "ZFLAGS=$(OCAMLLIBS) $(COQSRC)\n";
- if !opt="-opt" then
- print "COQFLAGS=-q $(OPT) $(COQLIBS)\n"
- else begin
- print "OPTCOQ=";
- print "$(OPT:-opt="; print !opt; print ")\n";
- print "COQFLAGS=-q $(OPTCOQ) $(COQLIBS)\n"
- end;
+ print "OPT="; if !opt = "-byte" then print "-byte"; print "\n";
+ print "COQFLAGS=-q $(OPT) $(COQLIBS)\n";
print "COQC=$(COQBIN)coqc\n";
- print "COQFULL=$(COQBIN)coqc $(FULLOPT) -q $(COQLIBS)\n";
print "GALLINA=gallina\n";
print "COQ2HTML=coq2html\n";
print "COQ2LATEX=coq2latex\n";