more robust locations (amending 7e11e96a922d) --- notably for cleanup() in build_release, after Admin/ been deleted;
authorwenzelm
Tue, 24 Jan 2023 21:27:10 +0100
changeset 77085 351eee493580
parent 77084 f9a858060836
child 77086 bd5045cd6ca9
more robust locations (amending 7e11e96a922d) --- notably for cleanup() in build_release, after Admin/ been deleted;
src/Pure/Admin/other_isabelle.scala
--- a/src/Pure/Admin/other_isabelle.scala	Tue Jan 24 20:48:28 2023 +0100
+++ b/src/Pure/Admin/other_isabelle.scala	Tue Jan 24 21:27:10 2023 +0100
@@ -51,9 +51,9 @@
   def expand_path(path: Path): Path = path.expand_env(settings)
   def bash_path(path: Path): String = Bash.string(expand_path(path).implode)
 
-  def isabelle_home_user: Path = expand_path(Path.explode("$ISABELLE_HOME_USER"))
+  val isabelle_home_user: Path = expand_path(Path.explode("$ISABELLE_HOME_USER"))
 
-  def etc: Path = expand_path(Path.explode("$ISABELLE_HOME_USER/etc"))
+  def etc: Path = isabelle_home_user + Path.explode("etc")
   def etc_settings: Path = etc + Path.explode("settings")
   def etc_preferences: Path = etc + Path.explode("preferences")