diff options
| -rw-r--r-- | ide/coqide_WIN32.ml.in | 3 | ||||
| -rw-r--r-- | ide/ide_win32_stubs.c | 16 |
2 files changed, 1 insertions, 18 deletions
diff --git a/ide/coqide_WIN32.ml.in b/ide/coqide_WIN32.ml.in index 8c4649fc39..0793a1cc1c 100644 --- a/ide/coqide_WIN32.ml.in +++ b/ide/coqide_WIN32.ml.in @@ -37,9 +37,8 @@ let reroute_stdout_stderr () = Unix.dup2 out_descr Unix.stdout; Unix.dup2 out_descr Unix.stderr -(* We also provide specific kill and interrupt functions. *) +(* We also provide a specific interrupt function. *) -external win32_kill : int -> unit = "win32_kill" external win32_interrupt : int -> unit = "win32_interrupt" let () = Coq.gio_channel_of_descr_socket := Glib.Io.channel_of_descr_socket; diff --git a/ide/ide_win32_stubs.c b/ide/ide_win32_stubs.c index c09bf37dee..f430c9f2b6 100644 --- a/ide/ide_win32_stubs.c +++ b/ide/ide_win32_stubs.c @@ -4,22 +4,6 @@ #include <caml/memory.h> #include <windows.h> -/* Win32 emulation of kill -9 */ - -/* The pid returned by Unix.create_process is actually a pseudo-pid, - made via a cast of the obtained HANDLE, (cf. win32unix/createprocess.c - in the sources of ocaml). Since we're still in the caller process, - we simply cast back to get an handle... - The 0 is the exit code we want for the terminated process. -*/ - -CAMLprim value win32_kill(value pseudopid) { - CAMLparam1(pseudopid); - TerminateProcess((HANDLE)(Long_val(pseudopid)), 0); - CAMLreturn(Val_unit); -} - - /* Win32 emulation of a kill -2 (SIGINT) */ /* This code rely of the fact that coqide is now without initial console. |