# HG changeset patch
# User wenzelm
# Date 1194898172 -3600
# Node ID 3326bd7ecd4835b09838a36eb2504b02008d2f96
# Parent  df27d19c35dd4857776c006a2a9ff2a66b0ca1ca
back to sigusr2, after Poly/ML 5.1 has been adapted;

diff -r df27d19c35dd -r 3326bd7ecd48 src/HOL/Tools/res_reconstruct.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));
 
diff -r df27d19c35dd -r 3326bd7ecd48 src/HOL/Tools/watcher.ML
--- 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