From 0bf85fbc04b448ede279842aec30659c9377969d Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Mon, 9 Jan 2017 16:43:07 +0100
Subject: Compile with debug information by default.

Addition of debug info can be prevented using -nodebug at configure
time.
---
 configure.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/configure.ml b/configure.ml
index f75bbb538c..9c22c52375 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))
@@ -337,6 +337,8 @@ let args_options = Arg.align [
     " Compiles only bytecode version of Coq";
   "-debug", Arg.Set Prefs.debug,
     " Add debugging information in the Coq executables";
+  "-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,
-- 
cgit v1.2.3