back to sigusr2, after Poly/ML 5.1 has been adapted;
authorwenzelm
Mon, 12 Nov 2007 21:09:32 +0100
changeset 25414 3326bd7ecd48
parent 25413 df27d19c35dd
child 25415 02884a4e1ac6
back to sigusr2, after Poly/ML 5.1 has been adapted;
src/HOL/Tools/res_reconstruct.ML
src/HOL/Tools/watcher.ML
--- a/src/HOL/Tools/res_reconstruct.ML	Mon Nov 12 20:10:34 2007 +0100
+++ b/src/HOL/Tools/res_reconstruct.ML	Mon Nov 12 21:09:32 2007 +0100
@@ -467,7 +467,7 @@
     TextIO.output (toParent, "Success.\n");
     TextIO.output (toParent, probfile ^ "\n");
     TextIO.flushOut toParent;
-    Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr1);
+    Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
     (*Give the parent time to respond before possibly sending another signal*)
     OS.Process.sleep (Time.fromMilliseconds 600)
   end;
@@ -603,7 +603,7 @@
   TextIO.output (toParent, probfile ^ "\n");
   TextIO.flushOut toParent;
   trace ("\nSignalled parent: " ^ msg ^ probfile);
-  Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr1);
+  Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
   (*Give the parent time to respond before possibly sending another signal*)
   OS.Process.sleep (Time.fromMilliseconds 600));
 
--- a/src/HOL/Tools/watcher.ML	Mon Nov 12 20:10:34 2007 +0100
+++ b/src/HOL/Tools/watcher.ML	Mon Nov 12 21:09:32 2007 +0100
@@ -407,7 +407,7 @@
 	       decr_watched())
        end
  in Output.debug (fn () => ("subgoals forked to createWatcher: "^ prems_string_of th));
-    IsaSignal.signal (IsaSignal.usr1, IsaSignal.SIG_HANDLE proofHandler);
+    IsaSignal.signal (IsaSignal.usr2, IsaSignal.SIG_HANDLE proofHandler);
     (childin, childout, childpid)
   end