proper path;
authorwenzelm
Fri, 22 Jan 2021 15:58:17 +0100
changeset 73173 91fc3b3df93f
parent 73172 fc828f64da5b
child 73174 ab3fa0abc119
proper path;
src/Pure/Admin/components.scala
--- a/src/Pure/Admin/components.scala	Thu Jan 21 16:10:43 2021 +0100
+++ b/src/Pure/Admin/components.scala	Fri Jan 22 15:58:17 2021 +0100
@@ -132,7 +132,7 @@
 
   /** manage user components **/
 
-  val components_path = Path.explode("$ISABELLE_HOME_USER/components")
+  val components_path = Path.explode("$ISABELLE_HOME_USER/etc/components")
 
   def read_components(): List[String] =
     if (components_path.is_file) Library.trim_split_lines(File.read(components_path))