| changeset 75497 | 0a5f7b5da16f |
| parent 75393 | 87ebf5a50283 |
| child 76883 | 186e07be32c3 |
--- a/src/Pure/Admin/afp.scala Mon May 30 20:58:45 2022 +0200 +++ b/src/Pure/Admin/afp.scala Mon May 30 22:34:45 2022 +0200 @@ -23,7 +23,9 @@ val force_partition1: List[String] = List("Category3", "HOL-ODE") - def init(options: Options, base_dir: Path = Path.explode("$AFP_BASE")): AFP = + val BASE: Path = Path.explode("$AFP_BASE") + + def init(options: Options, base_dir: Path = BASE): AFP = new AFP(options, base_dir)