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