# HG changeset patch
# User wenzelm
# Date 1222970341 -7200
# Node ID db8667d84dd2ff6c15ca54d3d779f6d61212df83
# Parent  dcc030b525838319cce8e74e61b97df058a450be
tracing: ignore failure of any kind;

diff -r dcc030b52583 -r db8667d84dd2 src/Pure/ML-Systems/multithreading_polyml.ML
--- a/src/Pure/ML-Systems/multithreading_polyml.ML	Thu Oct 02 19:59:00 2008 +0200
+++ b/src/Pure/ML-Systems/multithreading_polyml.ML	Thu Oct 02 19:59:01 2008 +0200
@@ -32,10 +32,11 @@
 (* options *)
 
 val trace = ref 0;
+
 fun tracing level msg =
-  if level <= ! trace
-  then (TextIO.output (TextIO.stdErr, (">>> " ^ msg () ^ "\n")); TextIO.flushOut TextIO.stdErr)
-  else ();
+  if level > ! trace then ()
+  else (TextIO.output (TextIO.stdErr, (">>> " ^ msg () ^ "\n")); TextIO.flushOut TextIO.stdErr)
+    handle _ (*sic*) => ();
 
 val available = true;