# HG changeset patch
# User wenzelm
# Date 1194894634 -3600
# Node ID df27d19c35dd4857776c006a2a9ff2a66b0ca1ca
# Parent  6f56f0350f6c0e06b842a6033cf088d8729e0d61
changed Posix.Signal.usr2 to Posix.Signal.usr1 to make it work with Poly/ML 5.1;

diff -r 6f56f0350f6c -r df27d19c35dd src/HOL/Tools/res_reconstruct.ML
--- a/src/HOL/Tools/res_reconstruct.ML	Mon Nov 12 19:02:32 2007 +0100
+++ b/src/HOL/Tools/res_reconstruct.ML	Mon Nov 12 20:10:34 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.usr2);
+    Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr1);
     (*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.usr2);
+  Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr1);
   (*Give the parent time to respond before possibly sending another signal*)
   OS.Process.sleep (Time.fromMilliseconds 600));
 
diff -r 6f56f0350f6c -r df27d19c35dd src/HOL/Tools/watcher.ML
--- a/src/HOL/Tools/watcher.ML	Mon Nov 12 19:02:32 2007 +0100
+++ b/src/HOL/Tools/watcher.ML	Mon Nov 12 20:10:34 2007 +0100
@@ -407,7 +407,7 @@
 	       decr_watched())
        end
  in Output.debug (fn () => ("subgoals forked to createWatcher: "^ prems_string_of th));
-    IsaSignal.signal (IsaSignal.usr2, IsaSignal.SIG_HANDLE proofHandler);
+    IsaSignal.signal (IsaSignal.usr1, IsaSignal.SIG_HANDLE proofHandler);
     (childin, childout, childpid)
   end