diff options
Diffstat (limited to 'config')
| -rw-r--r-- | config/Makefile.template | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/config/Makefile.template b/config/Makefile.template index f35af2b58..e5061ebe8 100644 --- a/config/Makefile.template +++ b/config/Makefile.template @@ -72,8 +72,9 @@ CAMLMKTOP="CAMLMKTOPEXEC" # Caml flags CAMLFLAGS=-rectypes CAMLANNOTATEFLAG -# Compilation debug flag +# Compilation debug flags CAMLDEBUG=COQDEBUGFLAG +CAMLDEBUGOPT=COQDEBUGFLAGOPT # User compilation flag USERFLAGS= |