equal
deleted
inserted
replaced
68 private val script_file = Isabelle_System.tmp_file("bash_script") |
68 private val script_file = Isabelle_System.tmp_file("bash_script") |
69 File.write(script_file, script) |
69 File.write(script_file, script) |
70 |
70 |
71 private val proc = |
71 private val proc = |
72 Isabelle_System.process( |
72 Isabelle_System.process( |
73 List(File.platform_path(Path.variable("ISABELLE_BASH_PROCESS")), "-", |
73 List(File.platform_path(Path.variable("ISABELLE_BASH_PROCESS")), |
74 File.standard_path(timing_file), "bash", File.standard_path(script_file)), |
74 File.standard_path(timing_file), "bash", File.standard_path(script_file)), |
75 cwd = cwd, env = env, redirect = redirect) |
75 cwd = cwd, env = env, redirect = redirect) |
76 |
76 |
77 |
77 |
78 // channels |
78 // channels |