equal
deleted
inserted
replaced
1013 |
1013 |
1014 progress.echo( |
1014 progress.echo( |
1015 (if (store_heap) "Building " else "Running ") + session_name + |
1015 (if (store_heap) "Building " else "Running ") + session_name + |
1016 if_proper(node_info.numa_node, " on " + node_info) + " ...") |
1016 if_proper(node_info.numa_node, " on " + node_info) + " ...") |
1017 |
1017 |
1018 store.clean_output(_database_server, session_name, session_init = true) |
|
1019 |
|
1020 val session = state.sessions(session_name) |
1018 val session = state.sessions(session_name) |
1021 |
1019 |
1022 val build = |
1020 val build = |
1023 Build_Job.start_session(build_context, session, progress, log, _database_server, |
1021 Build_Job.start_session(build_context, session, progress, log, _database_server, |
1024 build_deps.background(session_name), sources_shasum, input_shasum, node_info, store_heap) |
1022 build_deps.background(session_name), sources_shasum, input_shasum, node_info, store_heap) |