src/Pure/System/standard_system.scala
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