src/Pure/System/standard_system.scala
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: _*))
 }