system: writeln output, if available;

--- 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;