# HG changeset patch
# User wenzelm
# Date 1284833268 -7200
# Node ID 01aade784da9a1234633e75943ad32e61ae49b35
# Parent  7ed922d158272f73cbb89ee3e811364e38cdc3b0
raw_execute: let IOException pass-through unhindered (again);

diff -r 7ed922d15827 -r 01aade784da9 src/Pure/System/standard_system.scala
--- a/src/Pure/System/standard_system.scala	Sat Sep 18 19:38:27 2010 +0200
+++ b/src/Pure/System/standard_system.scala	Sat Sep 18 20:07:48 2010 +0200
@@ -132,9 +132,7 @@
       for ((x, y) <- env) proc.environment.put(x, y)
     }
     proc.redirectErrorStream(redirect)
-
-    try { proc.start }
-    catch { case e: IOException => error(e.getMessage) }
+    proc.start
   }
 
   def process_output(proc: Process): (String, Int) =
@@ -152,8 +150,8 @@
     (output, rc)
   }
 
-  def raw_exec(cwd: File, env: Map[String, String], redirect: Boolean, args: String*):
-    (String, Int) = process_output(raw_execute(cwd, env, redirect, args: _*))
+  def raw_exec(cwd: File, env: Map[String, String], redirect: Boolean, args: String*)
+    : (String, Int) = process_output(raw_execute(cwd, env, redirect, args: _*))
 }