# HG changeset patch
# User wenzelm
# Date 1708631691 -3600
# Node ID f25a6b4c3e41dc83b8186d124b341de03bc380d5
# Parent  4ded6d260db03abea1148f52fb312d721744962b
tuned;

diff -r 4ded6d260db0 -r f25a6b4c3e41 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