# HG changeset patch
# User wenzelm
# Date 1222681612 -7200
# Node ID 9aa3216e5f31e4324ea7d572b4004243d4efe077
# Parent  389c5e494605d18f8496d40b6e6620b80d922031
tuned comments;

diff -r 389c5e494605 -r 9aa3216e5f31 src/Pure/ML-Systems/multithreading_polyml.ML
--- a/src/Pure/ML-Systems/multithreading_polyml.ML	Mon Sep 29 11:46:47 2008 +0200
+++ b/src/Pure/ML-Systems/multithreading_polyml.ML	Mon Sep 29 11:46:52 2008 +0200
@@ -149,7 +149,7 @@
               if s = Posix.Signal.int then Signal
               else Result (256 + LargeWord.toInt (Posix.Signal.toWord s))
           | Posix.Process.W_STOPPED s => Result (512 + LargeWord.toInt (Posix.Signal.toWord s)));
-      in set_result res end handle _ => set_result (Result 2), []);
+      in set_result res end handle _ (*sic*) => set_result (Result 2), []);
 
     (*main thread -- proxy for interrupts*)
     fun kill n =