changeset 80056 | 9279e96eb34e |
parent 80055 | 42bc8ab751c1 |
child 80057 | 87f90735e6dd |
--- a/src/Pure/Admin/afp.scala Thu Mar 28 16:27:36 2024 +0100 +++ b/src/Pure/Admin/afp.scala Thu Mar 28 16:38:12 2024 +0100 @@ -18,7 +18,7 @@ def main_dir(base_dir: Path = BASE): Path = base_dir + Path.explode("thys") - def make_dirs(afp_root: Option[Path]): List[Path] = + def main_dirs(afp_root: Option[Path]): List[Path] = afp_root match { case None => Nil case Some(base_dir) => List(main_dir(base_dir = base_dir))