# HG changeset patch # User wenzelm # Date 1203177129 -3600 # Node ID 4ce22e7a81bdcaaf4b946d4dd93aa0edc0197b05 # Parent a7475459c7402b9bddbdf4d9d4b7cd045eda8ef9 removed spurious PolyML.makestring; diff -r a7475459c740 -r 4ce22e7a81bd src/Pure/General/system_process.ML --- a/src/Pure/General/system_process.ML Sat Feb 16 16:44:02 2008 +0100 +++ b/src/Pure/General/system_process.ML Sat Feb 16 16:52:09 2008 +0100 @@ -31,7 +31,6 @@ val status = Unix.reap proc; val rc = Unix.fromStatus status; in - tracing (PolyML.makestring (Unix.fromStatus status)); if rc = Unix.W_SIGNALED Posix.Signal.int orelse rc = Unix.W_EXITSTATUS 0wx82 then raise Interrupt else (Buffer.content output, if OS.Process.isSuccess status then 0 else 1)