equal
deleted
inserted
replaced
189 |
189 |
190 |
190 |
191 /* output log */ |
191 /* output log */ |
192 |
192 |
193 val log_path = |
193 val log_path = |
194 other_isabelle.isabelle_home_user + Path.explode("log") + |
194 other_isabelle.isabelle_home_user + |
195 Build_Log.log_path(BUILD_HISTORY, build_history_date, ml_platform, "M" + threads).ext("gz") |
195 Build_Log.log_subdir(build_history_date) + |
|
196 Build_Log.log_filename( |
|
197 BUILD_HISTORY, build_history_date, ml_platform, "M" + threads).ext("gz") |
196 |
198 |
197 val build_info = Build_Log.Log_File(log_path.base.implode, res.out_lines).parse_build_info() |
199 val build_info = Build_Log.Log_File(log_path.base.implode, res.out_lines).parse_build_info() |
198 |
200 |
199 val meta_info = |
201 val meta_info = |
200 List(Build_Log.Field.build_engine -> BUILD_HISTORY, |
202 List(Build_Log.Field.build_engine -> BUILD_HISTORY, |