# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1718025201 -7200
# Node ID e070eca8c7314b0c44b8400b58f8c12e9e3c1d0a
# Parent  b835b40f53ecedebd6a03290c479ba55ddc5b330
clarified;

diff -r b835b40f53ec -r e070eca8c731 src/Pure/Build/build_manager.scala
--- a/src/Pure/Build/build_manager.scala	Mon Jun 10 14:08:15 2024 +0200
+++ b/src/Pure/Build/build_manager.scala	Mon Jun 10 15:13:21 2024 +0200
@@ -1207,8 +1207,8 @@
     val base_dir = Path.explode(options.string("build_manager_dir"))
     val identifier = options.string("build_manager_identifier")
 
-    private val pending = base_dir + Path.basic("pending")
-    private val finished = base_dir + Path.basic("finished")
+    val pending = base_dir + Path.basic("pending")
+    val finished = base_dir + Path.basic("finished")
 
     def task_dir(task: Task) = pending + Path.basic(task.id.toString)
     def log_file(name: String): Path = finished + Path.explode(name)