diff options
| author | Gaëtan Gilbert | 2018-11-28 12:48:32 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-11-28 12:49:43 +0100 |
| commit | 8ea2e4100737794d3130e2bc341f5a1c6422082f (patch) | |
| tree | 59368077c9350c1a8d25b84abeba5402cba1c781 | |
| parent | 2e36fbcac4a04d4f29925ba09f441db6426b7af1 (diff) | |
coqide: Remove unused win32_kill C function
Unused since b0da879dc6abfca6b4e233b7469265a5cf52ce15 (see also
followup 4f554c88aa).
| -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. |