# HG changeset patch
# User wenzelm
# Date 1678811678 -3600
# Node ID 78913f29fc216df92a7248c0a0d6372b7e1b7158
# Parent  26bb79d17910dc214805ecbd0cbbfef78954afb4
tuned signature;

diff -r 26bb79d17910 -r 78913f29fc21 src/Pure/Tools/build_process.scala
--- a/src/Pure/Tools/build_process.scala	Tue Mar 14 17:09:52 2023 +0100
+++ b/src/Pure/Tools/build_process.scala	Tue Mar 14 17:34:38 2023 +0100
@@ -1066,22 +1066,23 @@
 
   /* build process roles */
 
-  final def is_session_name(job_name: String): Boolean = !Long_Name.is_qualified(job_name)
+  final def is_session_name(job_name: String): Boolean =
+    !Long_Name.is_qualified(job_name)
 
-  final def start_build(): Unit = synchronized_database {
+  protected final def start_build(): Unit = synchronized_database {
     for (db <- _database) {
       Build_Process.Data.start_build(db, build_uuid, build_context.ml_platform,
         build_context.sessions_structure.session_prefs, progress.stopped)
     }
   }
 
-  final def stop_build(): Unit = synchronized_database {
+  protected final def stop_build(): Unit = synchronized_database {
     for (db <- _database) {
       Build_Process.Data.stop_build(db, build_uuid)
     }
   }
 
-  final def start_worker(): Unit = synchronized_database {
+  protected final def start_worker(): Unit = synchronized_database {
     for (db <- _database) {
       val java = ProcessHandle.current()
       val java_pid = java.pid
@@ -1093,7 +1094,7 @@
     }
   }
 
-  final def stop_worker(): Unit = synchronized_database {
+  protected final def stop_worker(): Unit = synchronized_database {
     for (db <- _database) {
       Build_Process.Data.stamp_worker(db, worker_uuid, _state.serial, stop = true)
       _state = _state.set_workers(Build_Process.Data.read_workers(db))