--- 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: _*))
}