src/Pure/System/standard_system.scala
changeset 34258 e936d3c35ce0
parent 34219 d37cfca69887
child 34298 13e9f1f4acd9
equal deleted inserted replaced
34257:b5176fd9ab3c 34258:e936d3c35ce0
   130         proc.destroy
   130         proc.destroy
   131         Thread.interrupted
   131         Thread.interrupted
   132       }
   132       }
   133     (output, rc)
   133     (output, rc)
   134   }
   134   }
       
   135 
       
   136   def raw_exec(cwd: File, env: Map[String, String], redirect: Boolean, args: String*):
       
   137     (String, Int) = process_output(raw_execute(cwd, env, redirect, args: _*))
   135 }
   138 }
   136 
   139 
   137 
   140 
   138 class Standard_System
   141 class Standard_System
   139 {
   142 {