diff options
| author | letouzey | 2011-03-30 07:18:55 +0000 |
|---|---|---|
| committer | letouzey | 2011-03-30 07:18:55 +0000 |
| commit | a4355384effa75c4789e6ae0afb942206e985140 (patch) | |
| tree | df6561cec1f825aa22fa150dd742947a318688f3 /plugins/xml/xmlcommand.ml | |
| parent | bbe52c9e9f9e6929484d8041a5fbb0c56a6a3735 (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/xmlcommand.ml')
0 files changed, 0 insertions, 0 deletions