aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools/coq_makefile.ml4
diff options
context:
space:
mode:
Diffstat (limited to 'tools/coq_makefile.ml4')
-rw-r--r--tools/coq_makefile.ml45
1 files changed, 4 insertions, 1 deletions
diff --git a/tools/coq_makefile.ml4 b/tools/coq_makefile.ml4
index 1cd9d350c..891d41e6c 100644
--- a/tools/coq_makefile.ml4
+++ b/tools/coq_makefile.ml4
@@ -177,7 +177,10 @@ let variables l =
-I $(COQTOP)/contrib/ring -I $(COQTOP)/contrib/xml \\
-I $(CAMLP4LIB)\n";
print "ZFLAGS=$(OCAMLLIBS) $(COQSRC)\n";
- print "OPT="; if !opt = "-byte" then print "-byte"; print "\n";
+ if !opt = "-byte" then
+ print "override OPT=-byte\n"
+ else
+ print "OPT=\n";
print "COQFLAGS=-q $(OPT) $(COQLIBS)\n";
print "COQC=$(COQBIN)coqc\n";
print "GALLINA=gallina\n";