--- a/src/Pure/General/mercurial.scala Tue Oct 18 15:31:08 2016 +0200
+++ b/src/Pure/General/mercurial.scala Tue Oct 18 16:03:30 2016 +0200
@@ -16,7 +16,7 @@
/* command-line syntax */
def optional(s: String, prefix: String = ""): String =
- if (s == "") "" else " " + prefix + " " + File.bash_string(s)
+ if (s == "") "" else " " + prefix + " " + Bash.string(s)
def opt_flag(flag: String, b: Boolean): String = if (b) " " + flag else ""
def opt_rev(s: String): String = optional(s, "--rev")
@@ -40,7 +40,7 @@
case None => Isabelle_System.mkdirs(hg.root.dir)
case Some(ssh) => ssh.mkdirs(hg.root.dir)
}
- hg.command("clone", File.bash_string(source) + " " + File.bash_path(hg.root), options).check
+ hg.command("clone", Bash.string(source) + " " + File.bash_path(hg.root), options).check
hg
}