changeset 34258 | e936d3c35ce0 |
parent 34222 | d37cfca69887 |
child 34298 | 13e9f1f4acd9 |
1.1 --- a/src/Pure/System/standard_system.scala Mon Jan 04 22:35:32 2010 +0100 1.2 +++ b/src/Pure/System/standard_system.scala Mon Jan 04 22:43:07 2010 +0100 1.3 @@ -132,6 +132,9 @@ 1.4 } 1.5 (output, rc) 1.6 } 1.7 + 1.8 + def raw_exec(cwd: File, env: Map[String, String], redirect: Boolean, args: String*): 1.9 + (String, Int) = process_output(raw_execute(cwd, env, redirect, args: _*)) 1.10 } 1.11 1.12