--- 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