changeset 34258 | e936d3c35ce0 |
parent 34219 | d37cfca69887 |
child 34298 | 13e9f1f4acd9 |
--- a/src/Pure/System/standard_system.scala Mon Jan 04 22:35:32 2010 +0100 +++ b/src/Pure/System/standard_system.scala Mon Jan 04 22:43:07 2010 +0100 @@ -132,6 +132,9 @@ } (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: _*)) }