# 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)