equal
deleted
inserted
replaced
203 |
203 |
204 val build_start = Date.now() |
204 val build_start = Date.now() |
205 val build_args1 = List("-v", "-j" + processes) ::: build_args |
205 val build_args1 = List("-v", "-j" + processes) ::: build_args |
206 val build_result = |
206 val build_result = |
207 { |
207 { |
208 val progress1 = new Seq_Progress(progress, new File_Progress(build_out)) |
208 val other_isabelle1 = |
209 val other_isabelle1 = new Other_Isabelle(progress1, hg.root, isabelle_identifier) |
209 new Other_Isabelle(new File_Progress(build_out), hg.root, isabelle_identifier) |
210 other_isabelle1("build " + Bash.strings(build_args1), redirect = true, echo = verbose) |
210 other_isabelle1("build " + Bash.strings(build_args1), redirect = true, echo = true) |
211 } |
211 } |
212 val build_end = Date.now() |
212 val build_end = Date.now() |
213 |
213 |
214 val build_info: Build_Log.Build_Info = |
214 val build_info: Build_Log.Build_Info = |
215 Build_Log.Log_File(log_path.base.implode, build_result.out_lines). |
215 Build_Log.Log_File(log_path.base.implode, build_result.out_lines). |