# HG changeset patch
# User wenzelm
# Date 1205933159 -3600
# Node ID aa54cd3ddc9f933f070abce9ebfba0995bd99234
# Parent  92120667172f694e17d0b1d832f1fa89add61eca
system: writeln output, if available;

diff -r 92120667172f -r aa54cd3ddc9f src/Pure/General/secure.ML
--- a/src/Pure/General/secure.ML	Wed Mar 19 07:20:35 2008 +0100
+++ b/src/Pure/General/secure.ML	Wed Mar 19 14:25:59 2008 +0100
@@ -60,7 +60,11 @@
 val orig_system_out = system_out;
 
 fun system_out s = (secure_shell (); orig_system_out s);
-fun system s = #2 (system_out s);
+
+fun system s =
+  (case system_out s of
+    ("", rc) => rc
+  | (out, rc) => (writeln (perhaps (try (unsuffix "\n")) out); rc));
 
 end;