# HG changeset patch # User wenzelm # Date 1680965881 -7200 # Node ID 721b3278c8e47c7eb2b4374dd1e07b8dca3a3383 # Parent 4046731cfa6ceb3d8947d65402d783388c085b44 more direct Hg_Sync.check_directory via SSH operations; diff -r 4046731cfa6c -r 721b3278c8e4 src/Pure/General/mercurial.scala --- a/src/Pure/General/mercurial.scala Sat Apr 08 16:44:24 2023 +0200 +++ b/src/Pure/General/mercurial.scala Sat Apr 08 16:58:01 2023 +0200 @@ -126,6 +126,11 @@ val PATH_DIFF: Path = PATH + Path.explode("diff") val PATH_STAT: Path = PATH + Path.explode("stat") + def check_directory(root: Path, ssh: SSH.System = SSH.Local): Unit = + if (ssh.is_dir(root) && !ssh.is_dir(root + PATH) && ssh.read_dir(root).nonEmpty) { + error("No .hg_sync meta data in " + ssh.rsync_path(root)) + } + def is_directory(root: Path, ssh: SSH.System = SSH.Local): Boolean = ssh.is_dir(root + PATH) @@ -303,18 +308,12 @@ require(ssh.is_local, "local repository required") Isabelle_System.with_tmp_dir("sync") { tmp_dir => + Hg_Sync.check_directory(target, ssh = context.ssh) + val context0 = context.copy(progress = new Progress) Rsync.init(context0, target) - val list = - Rsync.exec(context0, list = true, - args = List("--", context.target(target, direct = true))) - .check.out_lines.filterNot(_.endsWith(" .")) - if (list.nonEmpty && !list.exists(_.endsWith(Hg_Sync._NAME))) { - error("No .hg_sync meta data in " + quote(context.target(target))) - } - val id_content = id(rev = rev) val is_changed = id_content.endsWith("+") val log_content = if (is_changed) "" else log(rev = rev, options = "-l1") diff -r 4046731cfa6c -r 721b3278c8e4 src/Pure/General/rsync.scala --- a/src/Pure/General/rsync.scala Sat Apr 08 16:44:24 2023 +0200 +++ b/src/Pure/General/rsync.scala Sat Apr 08 16:58:01 2023 +0200 @@ -33,7 +33,6 @@ prune_empty_dirs: Boolean = false, dry_run: Boolean = false, clean: Boolean = false, - list: Boolean = false, filter: List[String] = Nil, args: List[String] = Nil ): Process_Result = { @@ -45,7 +44,6 @@ (if (prune_empty_dirs) " --prune-empty-dirs" else "") + (if (dry_run) " --dry-run" else "") + (if (clean) " --delete-excluded" else "") + - (if (list) " --list-only --no-human-readable" else "") + filter.map(s => " --filter=" + Bash.string(s)).mkString + if_proper(args, " " + Bash.strings(args)) progress.bash(script, echo = true)