aboutsummaryrefslogtreecommitdiff
path: root/plugins/xml
diff options
context:
space:
mode:
authorletouzey2011-03-30 07:18:55 +0000
committerletouzey2011-03-30 07:18:55 +0000
commita4355384effa75c4789e6ae0afb942206e985140 (patch)
treedf6561cec1f825aa22fa150dd742947a318688f3 /plugins/xml
parentbbe52c9e9f9e6929484d8041a5fbb0c56a6a3735 (diff)
Ide_slave: better handling of Ctrl-C
- During input and output to coqide, we postpone Ctrl-C instead of ignoring them. For that we use Util.interrupt and Util.check_for_interrupt. - During evaluation of coqide requests, a Ctrl-C directly raises Sys.break, which is more reliable than waiting for the next Util.check_for_interrupt git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13939 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/xml')
0 files changed, 0 insertions, 0 deletions