diff options
| author |  notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-10-03 14:44:46 +0000 |
|---|---|---|
| committer | notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-10-03 14:44:46 +0000 |
| commit | e19ab99ea5b440dad9f80a57d18637f4d2d49811 (patch) | |
| tree | 3f9edf049dfc78c266a0afd4d68f2f2248c65239 /config/Makefile.template | |
| parent | 95483a55c228a0c3d9628a8b4e6cc45c84b8c894 (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/Makefile.template')
| -rw-r--r-- | config/Makefile.template | 3 |
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 |