changeset 74142 | 0f051404f487 |
parent 73279 | 37aff2142295 |
child 74147 | d030b988d470 |
--- a/src/Pure/Tools/generated_files.ML Sat Aug 07 21:25:47 2021 +0200 +++ b/src/Pure/Tools/generated_files.ML Sat Aug 07 22:23:37 2021 +0200 @@ -332,7 +332,7 @@ (* execute compiler -- auxiliary *) fun execute dir title compile = - Isabelle_System.bash_process ("cd " ^ File.bash_path dir ^ " && " ^ compile) + Isabelle_System.bash_process_script ("cd " ^ File.bash_path dir ^ " && " ^ compile) |> Process_Result.check |> Process_Result.out handle ERROR msg =>