# HG changeset patch
# User wenzelm
# Date 1622917225 -7200
# Node ID c8b4a4f69068d1c423a12e299e16e82789c0bbdf
# Parent  11f611494766a16eb4bfbfdf72fd460f3527669b
clarified check (refining fc828f64da5b): etc/settings or etc/components is not strictly required according to "init_component", and notable components only have session ROOTS (e.g. AFP/thys);

diff -r 11f611494766 -r c8b4a4f69068 src/Pure/Admin/components.scala
--- a/src/Pure/Admin/components.scala	Sat Jun 05 20:15:06 2021 +0200
+++ b/src/Pure/Admin/components.scala	Sat Jun 05 20:20:25 2021 +0200
@@ -152,7 +152,7 @@
   def update_components(add: Boolean, path0: Path, progress: Progress = new Progress): Unit =
   {
     val path = path0.expand.absolute
-    if (!check_dir(path)) error("Bad component directory: " + path)
+    if (!check_dir(path) && !Sessions.is_session_dir(path)) error("Bad component directory: " + path)
 
     val lines1 = read_components()
     val lines2 =
diff -r 11f611494766 -r c8b4a4f69068 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Sat Jun 05 20:15:06 2021 +0200
+++ b/src/Pure/Thy/sessions.scala	Sat Jun 05 20:20:25 2021 +0200
@@ -1014,7 +1014,7 @@
 
   /* load sessions from certain directories */
 
-  private def is_session_dir(dir: Path): Boolean =
+  def is_session_dir(dir: Path): Boolean =
     (dir + ROOT).is_file || (dir + ROOTS).is_file
 
   private def check_session_dir(dir: Path): Path =