# HG changeset patch
# User wenzelm
# Date 1674592030 -3600
# Node ID 351eee493580dc0d076eba358ada505572e0f4c6
# Parent  f9a858060836ef39c7f4a5149b97ab12c5a943d1
more robust locations (amending 7e11e96a922d) --- notably for cleanup() in build_release, after Admin/ been deleted;

diff -r f9a858060836 -r 351eee493580 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")