# HG changeset patch
# User wenzelm
# Date 1622916906 -7200
# Node ID 11f611494766a16eb4bfbfdf72fd460f3527669b
# Parent  90b64197bafd6f8bad4b87d94cfbae13d73ea10f
tuned;

diff -r 90b64197bafd -r 11f611494766 src/Pure/Admin/components.scala
--- a/src/Pure/Admin/components.scala	Sat Jun 05 19:21:29 2021 +0200
+++ b/src/Pure/Admin/components.scala	Sat Jun 05 20:15:06 2021 +0200
@@ -152,8 +152,7 @@
   def update_components(add: Boolean, path0: Path, progress: Progress = new Progress): Unit =
   {
     val path = path0.expand.absolute
-    if (!(path + Path.explode("etc/settings")).is_file &&
-        !(path + Path.explode("etc/components")).is_file) error("Bad component directory: " + path)
+    if (!check_dir(path)) error("Bad component directory: " + path)
 
     val lines1 = read_components()
     val lines2 =