# HG changeset patch # User wenzelm # Date 1675007357 -3600 # Node ID 515b6aaede327fca57f4a80bfb74da4333fd860c # Parent 523839d6d8fff3be838bbf1656eb3b5cefdcf93b enable clean_components by default: it saves a lot of local disk space, notably on virtual nodes; diff -r 523839d6d8ff -r 515b6aaede32 src/Pure/Admin/isabelle_cronjob.scala --- a/src/Pure/Admin/isabelle_cronjob.scala Sat Jan 28 22:31:40 2023 +0100 +++ b/src/Pure/Admin/isabelle_cronjob.scala Sun Jan 29 16:49:17 2023 +0100 @@ -141,7 +141,7 @@ history: Int = 0, history_base: String = "build_history_base", components_base: String = Components.dynamic_components_base, - clean_components: Boolean = false, + clean_components: Boolean = true, java_heap: String = "", options: String = "", args: String = "",