diff options
author | 2011-03-23 17:18:55 +0000 | |
---|---|---|
committer | 2011-03-23 17:18:55 +0000 | |
commit | 461798eeecfd2a59159fb9666874d8ea14209624 (patch) | |
tree | 5e8bc059ef5743622fa1fbbdf45145e2a2d23294 /Makefile.common | |
parent | 150f9c3cfd32e1e0ed71d11644614a6cab1621a7 (diff) |
Ide: experimentally allow coqide to interrupt or kill coqtop
- We now use create_process instead of open_process, and stores
the answered pid.
- The "Stop" button now sends a Sigint signal to this coqtop pid.
- The "Goto Start" button now works even if a computation is ongoing,
a new process is spawned and the previous one is killed -9, and
then a waitpid is done to avoid having zombies around.
Note that currently a vm_compute won't be stopped by a "Stop",
but only by a "Goto Start". This can be quite confusing. How to
properly document that "Goto Start" has the side effect of being
a kill ? Maybe we could check someday if the Ctrl-C has been
successful, and kill -9 if not ? Or maybe make coqide aware
of a flag "we_are_vm_computing" and then kill -9 instead of Ctrl-C
in this case ?
TODO:
- for the moment a forced "Goto Start" displays an unfriendly anomaly
- check if all this works under Windows (probably but not sure).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13926 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'Makefile.common')
0 files changed, 0 insertions, 0 deletions