aboutsummaryrefslogtreecommitdiffhomepage
path: root/config
diff options
context:
space:
mode:
authorGravatar glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7>2009-02-11 12:46:19 +0000
committerGravatar glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7>2009-02-11 12:46:19 +0000
commitd4cebff2033b0f68162feaa118cb5e43a9277fe1 (patch)
tree7b707e127638d85234f3fca8e284948c55699bbf /config
parentb0f53dde478905a69982948d69eab2f025c8b14a (diff)
Add -coqtoolsbyteflags and -custom to ./configure...
...and use -custom by default on Windows and MacOS (backport r11895) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11913 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'config')
-rw-r--r--config/Makefile.template1
1 files changed, 1 insertions, 0 deletions
diff --git a/config/Makefile.template b/config/Makefile.template
index 35e2a2d7d..6f9fac3c1 100644
--- a/config/Makefile.template
+++ b/config/Makefile.template
@@ -23,6 +23,7 @@ LOCAL=LOCALINSTALLATION
# Bytecode link flags for VM ("-custom" or "-dllib -lcoqrun")
COQRUNBYTEFLAGS=XCOQRUNBYTEFLAGS
+COQTOOLSBYTEFLAGS=XCOQTOOLSBYTEFLAGS
BUILDLDPATH=
# Paths for true installation