unused;
authorwenzelm
Sun, 21 Feb 2021 11:53:05 +0100
changeset 73266 d6a664daa285
parent 73265 76c9fcf80f96
child 73267 1d610d5524ff
unused;
src/Pure/System/kill.ML
--- a/src/Pure/System/kill.ML	Sun Feb 21 00:49:09 2021 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,59 +0,0 @@
-(*  Title:      Pure/System/kill.ML
-    Author:     Makarius
-
-Kill external process group.
-*)
-
-signature KILL =
-sig
-  type signal
-  val SIGNONE: signal
-  val SIGINT: signal
-  val SIGTERM: signal
-  val SIGKILL: signal
-  val kill_group: int -> signal -> bool
-end;
-
-if ML_System.platform_is_windows then ML
-\<open>
-structure Kill: KILL =
-struct
-
-type signal = string;
-
-val SIGNONE = "0";
-val SIGINT = "INT";
-val SIGTERM = "TERM";
-val SIGKILL = "KILL";
-
-fun kill_group pid s =
-  let
-    val cmd = getenv_strict "CYGWIN_ROOT" ^ "\\bin\\bash.exe";
-    val arg = "kill -" ^ s ^ " -" ^ string_of_int pid;
-  in
-    OS.Process.isSuccess (Windows.simpleExecute ("", quote cmd ^ " -c " ^ quote arg))
-      handle OS.SysErr _ => false
-  end;
-
-end;
-\<close>
-else ML
-\<open>
-structure Kill: KILL =
-struct
-
-type signal = Posix.Signal.signal;
-
-val SIGNONE = Posix.Signal.fromWord 0w0;
-val SIGINT = Posix.Signal.int;
-val SIGTERM = Posix.Signal.term;
-val SIGKILL = Posix.Signal.kill;
-
-fun kill_group pid s =
-  let
-    val arg = Posix.Process.K_GROUP (Posix.Process.wordToPid (LargeWord.fromInt pid));
-    val _ = Posix.Process.kill (arg, s);
-  in true end handle OS.SysErr _ => false;
-
-end;
-\<close>