--- 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))
--- a/src/Pure/Build/build.scala Thu Mar 28 16:27:36 2024 +0100
+++ b/src/Pure/Build/build.scala Thu Mar 28 16:38:12 2024 +0100
@@ -191,7 +191,7 @@
/* session selection and dependencies */
val full_sessions =
- Sessions.load_structure(build_options, dirs = AFP.make_dirs(afp_root) ::: dirs,
+ Sessions.load_structure(build_options, dirs = AFP.main_dirs(afp_root) ::: dirs,
select_dirs = select_dirs, infos = infos, augment_options = augment_options)
val full_sessions_selection = full_sessions.imports_selection(selection)
@@ -633,7 +633,7 @@
val build_master = find_builds(build_database, build_id, builds.filter(_.active))
val sessions_structure =
- Sessions.load_structure(build_options, dirs = AFP.make_dirs(afp_root) ::: dirs).
+ Sessions.load_structure(build_options, dirs = AFP.main_dirs(afp_root) ::: dirs).
selection(Sessions.Selection(sessions = build_master.sessions))
val build_deps =
--- a/src/Pure/Build/build_schedule.scala Thu Mar 28 16:27:36 2024 +0100
+++ b/src/Pure/Build/build_schedule.scala Thu Mar 28 16:38:12 2024 +0100
@@ -1483,7 +1483,7 @@
host_database: SQL.Database
): Schedule = {
val full_sessions =
- Sessions.load_structure(build_options, dirs = AFP.make_dirs(afp_root) ::: dirs,
+ Sessions.load_structure(build_options, dirs = AFP.main_dirs(afp_root) ::: dirs,
select_dirs = select_dirs, infos = infos, augment_options = augment_options)
val build_deps =