aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/coqide.mli
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-12-07 15:19:07 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-12-07 15:19:07 +0000
commit9555637d4b54e229e604db0bc8777564edd27691 (patch)
tree4e6c44eb707852e96969fb6d83069c86bdf55ba5 /ide/coqide.mli
parent10d19da7aec5061cc19b09c06b619d10bda6b289 (diff)
Coqide: better handling of gtk messages + fix win32 stdout/stderr rerouting
We now try harder to handle ourselves gtk messages (e.g. Gtk-WARNING ...). This way, we could reroute them nicely in w32, and pop-up the critical ones. Moreover, the code rerouting debug messages to a log file in w32 was using !Ideutils.debug before its initialization. Now, when a log file is used, its name is displayed in the about messages. Btw, some code cleaning in coqide_main git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16037 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'ide/coqide.mli')
-rw-r--r--ide/coqide.mli3
1 files changed, 3 insertions, 0 deletions
diff --git a/ide/coqide.mli b/ide/coqide.mli
index aba75be4b..ca5396950 100644
--- a/ide/coqide.mli
+++ b/ide/coqide.mli
@@ -12,6 +12,9 @@
no /bin/sh when using create_process instead of open_process. *)
val sup_args : string list ref
+(** In debug mode under win32, messages are written to a log file *)
+val logfile : string option ref
+
(** Filter the argv from coqide specific options, and set
Minilib.coqtop_path accordingly *)
val read_coqide_args : string list -> string list