aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7>2011-11-18 14:11:28 +0000
committerGravatar pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7>2011-11-18 14:11:28 +0000
commitd85069058adc3b1a50e4d9d758f53e57453f0cbf (patch)
tree35aaaac0947131f947e364ef9ce9893b0ff104b5
parentec0c502f5c6920c2fd59a926c9de050cdf7780e1 (diff)
Coqide -debug only printed Coqtop information.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14680 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r--ide/coqide.ml3
-rw-r--r--ide/ideutils.ml2
2 files changed, 4 insertions, 1 deletions
diff --git a/ide/coqide.ml b/ide/coqide.ml
index e6968c51c..899d0d6ca 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -2914,6 +2914,9 @@ let read_coqide_args argv =
if coqtop = "" then filter_coqtop prog project_files out args
else
(output_string stderr "Error: multiple -coqtop options"; exit 1)
+ | "-debug" :: args ->
+ Ideutils.debug := true;
+ filter_coqtop coqtop project_files ("-debug"::out) args
| "-f" :: file :: args ->
filter_coqtop coqtop
((Minilib.canonical_path_name (Filename.dirname file),
diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index 71ff87f00..1cf24948e 100644
--- a/ide/ideutils.ml
+++ b/ide/ideutils.ml
@@ -29,7 +29,7 @@ let set_location = ref (function s -> failwith "not ready")
let pbar = GRange.progress_bar ~pulse_step:0.2 ()
-let debug = Flags.debug
+let debug = ref (false)
let prerr_endline s =
if !debug then try prerr_endline s;flush stderr with _ -> ()