changed Posix.Signal.usr2 to Posix.Signal.usr1 to make it work with Poly/ML 5.1;
authorwenzelm
Mon, 12 Nov 2007 20:10:34 +0100
changeset 25413 df27d19c35dd
parent 25412 6f56f0350f6c
child 25414 3326bd7ecd48
changed Posix.Signal.usr2 to Posix.Signal.usr1 to make it work with Poly/ML 5.1;
src/HOL/Tools/res_reconstruct.ML
src/HOL/Tools/watcher.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));
 
--- 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