# HG changeset patch
# User wenzelm
# Date 1669891005 -3600
# Node ID c7996b073524c48db1a8b705ee8056d37cba8a39
# Parent  a82fc7755ba5c0e993eb00cb3f254b10a451b155
clarified check: allow to remove bad directories;

diff -r a82fc7755ba5 -r c7996b073524 src/Pure/System/components.scala
--- a/src/Pure/System/components.scala	Thu Dec 01 11:32:59 2022 +0100
+++ b/src/Pure/System/components.scala	Thu Dec 01 11:36:45 2022 +0100
@@ -180,7 +180,7 @@
 
   def update_components(add: Boolean, path0: Path, progress: Progress = new Progress): Unit = {
     val path = path0.expand.absolute
-    Directory(path).check
+    if (add) Directory(path).check
 
     val lines1 = read_components()
     val lines2 =