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