author | wenzelm |
Fri, 22 Jan 2021 15:58:17 +0100 | |
changeset 73173 | 91fc3b3df93f |
parent 73172 | fc828f64da5b |
child 73174 | ab3fa0abc119 |
--- 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))