src/HOL/Tools/res_reconstruct.ML
changeset 25413 df27d19c35dd
parent 25086 729f9aad1f50
child 25414 3326bd7ecd48
--- 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));