src/Pure/Admin/afp.scala
changeset 78417 01f61cf796e0
parent 76883 186e07be32c3
child 78420 c157af5f346e
--- a/src/Pure/Admin/afp.scala	Thu Jul 20 12:29:57 2023 +0200
+++ b/src/Pure/Admin/afp.scala	Thu Jul 20 12:38:00 2023 +0200
@@ -25,6 +25,8 @@
 
   val BASE: Path = Path.explode("$AFP_BASE")
 
+  def main_dir(base_dir: Path = BASE): Path = base_dir + Path.explode("thys")
+
   def init(options: Options, base_dir: Path = BASE): AFP =
     new AFP(options, base_dir)
 
@@ -68,7 +70,7 @@
 class AFP private(options: Options, val base_dir: Path) {
   override def toString: String = base_dir.expand.toString
 
-  val main_dir: Path = base_dir + Path.explode("thys")
+  val main_dir: Path = AFP.main_dir(base_dir = base_dir)
 
 
   /* metadata */