tuned;
authorwenzelm
Sat, 05 Jun 2021 20:15:06 +0200
changeset 73813 11f611494766
parent 73812 90b64197bafd
child 73814 c8b4a4f69068
tuned;
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 =