aboutsummaryrefslogtreecommitdiffhomepage
path: root/config
diff options
context:
space:
mode:
authorGravatar filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7>2000-05-03 22:39:27 +0000
committerGravatar filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7>2000-05-03 22:39:27 +0000
commit432bcaee29481bf9a26e890b8c6ad893cb65c4de (patch)
tree335918ac348b4302dc14d2274943e1a2177dbe5c /config
parentb1512d41c3d7065eb76eec0014376ad144414fb8 (diff)
compilation bytecode / native :
- script de configuration - Makefile - simplification de coqmktop - option -opt de coqc git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@413 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'config')
-rw-r--r--config/Makefile.template4
1 files changed, 2 insertions, 2 deletions
diff --git a/config/Makefile.template b/config/Makefile.template
index 6ae9ca84a..52c054372 100644
--- a/config/Makefile.template
+++ b/config/Makefile.template
@@ -59,8 +59,8 @@ CAMLDEBUG=COQDEBUGFLAG
# Compilation profile flag
CAMLTIMEPROF=COQPROFILEFLAG
-# Compilation of tools: bytecode (=byte) or native (=opt)
-COQTOOLS=COQTOOLSFLAG
+# The best compiler: native (=opt) or bytecode (=byte) if no native compiler
+BEST=BESTCOMPILER
# For Camlp4 use
P4=$(COQTOP)/bin/$(ARCH)/call_camlp4 -I $(COQTOP)/src/parsing