src/Pure/System/standard_system.scala
changeset 39522 01aade784da9
parent 38264 205b74a1bb18
child 39578 b75164153c37
--- 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: _*))
 }