aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev/tools
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 /dev/tools
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 'dev/tools')
0 files changed, 0 insertions, 0 deletions