aboutsummaryrefslogtreecommitdiffhomepage
path: root/configure.ml
diff options
context:
space:
mode:
Diffstat (limited to 'configure.ml')
-rw-r--r--configure.ml6
1 files changed, 4 insertions, 2 deletions
diff --git a/configure.ml b/configure.ml
index 48e167c99..e71136751 100644
--- a/configure.ml
+++ b/configure.ml
@@ -261,7 +261,7 @@ module Prefs = struct
let withdoc = ref false
let geoproof = ref false
let byteonly = ref false
- let debug = ref false
+ let debug = ref true
let profile = ref false
let annotate = ref false
let nativecompiler = ref (not (os_type_win32 || os_type_cygwin))
@@ -336,7 +336,9 @@ let args_options = Arg.align [
"-byteonly", Arg.Set Prefs.byteonly,
" Compiles only bytecode version of Coq";
"-debug", Arg.Set Prefs.debug,
- " Add debugging information in the Coq executables";
+ " Deprecated";
+ "-nodebug", Arg.Clear Prefs.debug,
+ " Do not add debugging information in the Coq executables";
"-profile", Arg.Set Prefs.profile,
" Add profiling information in the Coq executables";
"-annotate", Arg.Set Prefs.annotate,