tuned;
authorwenzelm
Thu, 22 Feb 2024 20:54:51 +0100
changeset 79708 f25a6b4c3e41
parent 79707 4ded6d260db0
child 79709 90fbcdafb34e
tuned;
src/Pure/Build/store.scala
--- a/src/Pure/Build/store.scala	Thu Feb 22 20:37:53 2024 +0100
+++ b/src/Pure/Build/store.scala	Thu Feb 22 20:54:51 2024 +0100
@@ -298,6 +298,10 @@
     if (system_heaps) List(system_output_dir)
     else List(user_output_dir, system_output_dir)
 
+  val clean_dirs: List[Path] =
+    if (system_heaps) List(user_output_dir, system_output_dir)
+    else List(user_output_dir)
+
   def presentation_dir: Path =
     if (system_heaps) Path.explode("$ISABELLE_BROWSER_INFO_SYSTEM")
     else Path.explode("$ISABELLE_BROWSER_INFO")
@@ -437,8 +441,7 @@
 
     val del =
       for {
-        dir <-
-          (if (system_heaps) List(user_output_dir, system_output_dir) else List(user_output_dir))
+        dir <- clean_dirs
         file <- List(Store.heap(name), Store.log_db(name), Store.log(name), Store.log_gz(name))
         path = dir + file if path.is_file
       } yield path.file.delete