aboutsummaryrefslogtreecommitdiffhomepage
path: root/configure.ml
diff options
context:
space:
mode:
Diffstat (limited to 'configure.ml')
-rw-r--r--configure.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/configure.ml b/configure.ml
index 9c22c5237..6d96e614d 100644
--- a/configure.ml
+++ b/configure.ml
@@ -336,7 +336,7 @@ 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,