--- 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)
--- a/src/Pure/Admin/sync_repos.scala Mon May 30 20:58:45 2022 +0200
+++ b/src/Pure/Admin/sync_repos.scala Mon May 30 22:34:45 2022 +0200
@@ -64,7 +64,7 @@
Usage: isabelle sync_repos [OPTIONS] TARGET
Options are:
- -A ROOT include AFP with given root directory
+ -A ROOT include AFP with given root directory (":" for """ + AFP.BASE.implode + """)
-J preserve *.jar files
-C clean all unknown/ignored files on target
(implies -n for testing; use option -f to confirm)
@@ -81,13 +81,13 @@
* quick testing
- isabelle sync_repos -A '$AFP_BASE' -J -C testmachine:test/isabelle_afp
+ isabelle sync_repos -A: -J -C testmachine:test/isabelle_afp
* accurate testing
- isabelle sync_repos -A '$AFP_BASE' -T -C testmachine:test/isabelle_afp
+ isabelle sync_repos -A: -T -C testmachine:test/isabelle_afp
""",
- "A:" -> (arg => afp_root = Some(Path.explode(arg))),
+ "A:" -> (arg => afp_root = Some(if (arg == ":") AFP.BASE else Path.explode(arg))),
"J" -> (_ => preserve_jars = true),
"C" -> { _ => clean = true; dry_run = true },
"T" -> (_ => thorough = true),