aboutsummaryrefslogtreecommitdiffhomepage
path: root/config
diff options
context:
space:
mode:
authorGravatar notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7>2007-10-03 14:44:46 +0000
committerGravatar notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7>2007-10-03 14:44:46 +0000
commite19ab99ea5b440dad9f80a57d18637f4d2d49811 (patch)
tree3f9edf049dfc78c266a0afd4d68f2f2248c65239 /config
parent95483a55c228a0c3d9628a8b4e6cc45c84b8c894 (diff)
Compilation sous windows
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10171 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'config')
-rw-r--r--config/Makefile.template3
1 files changed, 3 insertions, 0 deletions
diff --git a/config/Makefile.template b/config/Makefile.template
index 4e2cc42b0..f99c7cfbc 100644
--- a/config/Makefile.template
+++ b/config/Makefile.template
@@ -73,6 +73,9 @@ CAMLDEBUG=COQDEBUGFLAG
# User compilation flag
USERFLAGS=
+# Flags for GCC
+CFLAGS=CCOMPILEFLAGS
+
# Compilation profile flag
CAMLTIMEPROF=COQPROFILEFLAG