author | wenzelm |
Wed, 14 Dec 2016 10:29:47 +0100 | |
changeset 64562 | e154ec4e3eac |
parent 64557 | 37074e22e8be |
child 64563 | 20e361014f55 |
--- a/src/Pure/Concurrent/multithreading.ML Tue Dec 13 23:29:54 2016 +0100 +++ b/src/Pure/Concurrent/multithreading.ML Wed Dec 14 10:29:47 2016 +0100 @@ -61,7 +61,7 @@ val trace = ref 0; fun tracing level msg = - if level > ! trace then () + if ! trace < level then () else Thread_Attributes.uninterruptible (fn _ => fn () => (TextIO.output (TextIO.stdErr, (">>> " ^ msg () ^ "\n")); TextIO.flushOut TextIO.stdErr) handle _ (*sic*) => ()) ();