src/Tools/cache_io.ML
changeset 43850 7f2cbc713344
parent 42127 8223e7f4b0da
child 50316 7bdc53fb7282
     1.1 --- a/src/Tools/cache_io.ML	Sat Jul 16 20:14:58 2011 +0200
     1.2 +++ b/src/Tools/cache_io.ML	Sat Jul 16 20:52:41 2011 +0200
     1.3 @@ -40,7 +40,7 @@
     1.4  fun raw_run make_cmd str in_path out_path =
     1.5    let
     1.6      val _ = File.write in_path str
     1.7 -    val (out2, rc) = bash_output (make_cmd in_path out_path)
     1.8 +    val (out2, rc) = Isabelle_System.bash_output (make_cmd in_path out_path)
     1.9      val out1 = the_default [] (try (rev o File.fold_lines cons out_path) [])
    1.10    in {output=split_lines out2, redirected_output=out1, return_code=rc} end
    1.11