aboutsummaryrefslogtreecommitdiff
path: root/ide/ideutils.ml
diff options
context:
space:
mode:
authormonate2003-02-26 16:32:01 +0000
committermonate2003-02-26 16:32:01 +0000
commit7b9c7dd7da681c3d8c37473385c0bc1bd5d998f8 (patch)
tree847bb1348e3eb6020eaa191549787d7fb2bb3c6b /ide/ideutils.ml
parentb4911b4581e43804893e649827804a9ff3f3bc59 (diff)
coqide: preliminary support for mnemonics. Edit menu. Context help now works properly.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3705 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'ide/ideutils.ml')
-rw-r--r--ide/ideutils.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index 52f7b3d28a..f0a0b4181c 100644
--- a/ide/ideutils.ml
+++ b/ide/ideutils.ml
@@ -22,7 +22,7 @@ let process_pending () =
ignore (Glib.Main.iteration false)
done
-let debug = ref false
+let debug = ref true
let prerr_endline s =
if !debug then prerr_endline s else ()
@@ -49,7 +49,7 @@ let try_export file_name s =
with e -> prerr_endline (Printexc.to_string e)
let browse url =
- let l,r = Preferences.current.cmd_browse in
+ let l,r = current.cmd_browse in
ignore (Sys.command (l ^ url ^ r))
let url_for_keyword =