changeset 74147 | d030b988d470 |
parent 74142 | 0f051404f487 |
child 74373 | 6e4093927dbb |
--- a/src/Pure/Tools/generated_files.ML Thu Aug 12 13:55:45 2021 +0200 +++ b/src/Pure/Tools/generated_files.ML Thu Aug 12 14:18:46 2021 +0200 @@ -332,7 +332,7 @@ (* execute compiler -- auxiliary *) fun execute dir title compile = - Isabelle_System.bash_process_script ("cd " ^ File.bash_path dir ^ " && " ^ compile) + Isabelle_System.bash_process (Bash.script compile |> Bash.cwd dir) |> Process_Result.check |> Process_Result.out handle ERROR msg =>