--- 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
=================================================
--- 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 {
--- 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)