diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-04-21 16:12:57 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-04-21 16:12:57 +0000 |
| commit | e1d0e7cd11cfe63f4741274f6d94f07887f32ffe (patch) | |
| tree | 1011840a8fc280819449d00ee11500b7bb6ab727 /ide/coq.ml | |
| parent | c9febd2450c40dbc46182662ccdc1567050d0222 (diff) | |
Coqide: a special kill function for win32
This is implemented as a C external launching the TerminateProcess
of the Win32 API. This should be considered as quite experimental
(cf. the way we handle pid in the comment of ide_win32_stubs.c).
I don't know how to emulate an interrupt (Ctrl-C), for now the two
button "Restart" and "Interrupt" have the same semantics on win32
(kill the subprocess and start at top).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14044 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'ide/coq.ml')
| -rw-r--r-- | ide/coq.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/ide/coq.ml b/ide/coq.ml index d595fbc91..1d67e8ee7 100644 --- a/ide/coq.ml +++ b/ide/coq.ml @@ -167,9 +167,11 @@ let break_coqtop coqtop = try Unix.kill coqtop.pid Sys.sigint with _ -> prerr_endline "Error while sending Ctrl-C" +let killer = ref (fun pid -> Unix.kill pid Sys.sigkill) + let blocking_kill pid = begin - try Unix.kill pid Sys.sigkill; + try !killer pid with _ -> prerr_endline "Kill -9 failed. Process already terminated ?" end; try |