# HG changeset patch
# User wenzelm
# Date 1653852748 -7200
# Node ID 6c93c13ba3c87036ad4ced73af382f4adb4010ff
# Parent  4363ad65ad361f66ced76c13feb3d72d5180ba29
more robust: local repository required;

diff -r 4363ad65ad36 -r 6c93c13ba3c8 NEWS
--- a/NEWS	Sun May 29 20:57:10 2022 +0200
+++ b/NEWS	Sun May 29 21:32:28 2022 +0200
@@ -1,3 +1,4 @@
+
 Isabelle NEWS -- history of user-relevant changes
 =================================================
 
diff -r 4363ad65ad36 -r 6c93c13ba3c8 src/Pure/General/mercurial.scala
--- a/src/Pure/General/mercurial.scala	Sun May 29 20:57:10 2022 +0200
+++ b/src/Pure/General/mercurial.scala	Sun May 29 21:32:28 2022 +0200
@@ -259,6 +259,8 @@
       filter: List[String] = Nil,
       rev: String = ""
     ): Unit = {
+      require(ssh == SSH.Local, "local repository required")
+
       Isabelle_System.with_tmp_dir("rsync") { tmp_dir =>
         val (options, source) =
           if (rev.isEmpty) {
@@ -267,7 +269,7 @@
             File.write(exclude_path, cat_lines((".hg" :: exclude).map("/" + _)))
 
             val options = List("--exclude-from=" + exclude_path.implode)
-            val source = ssh.rsync_url + root.expand.implode
+            val source = File.standard_path(root)
             (options, source)
           }
           else {
diff -r 4363ad65ad36 -r 6c93c13ba3c8 src/Pure/General/ssh.scala
--- a/src/Pure/General/ssh.scala	Sun May 29 20:57:10 2022 +0200
+++ b/src/Pure/General/ssh.scala	Sun May 29 21:32:28 2022 +0200
@@ -328,9 +328,6 @@
     override def hg_url: String =
       "ssh://" + user_prefix(nominal_user) + nominal_host + "/"
 
-    override def rsync_url: String = ""
-      user_prefix(nominal_user) + nominal_host + ":" + port_suffix(port, suffix = "") + "/"
-
     override def toString: String =
       user_prefix(session.getUserName) + host + port_suffix(port) +
       (if (session.isConnected) "" else " (disconnected)")
@@ -491,7 +488,6 @@
     def close(): Unit = ()
 
     def hg_url: String = ""
-    def rsync_url: String = ""
 
     def expand_path(path: Path): Path = path.expand
     def bash_path(path: Path): String = File.bash_path(path)