# HG changeset patch # User wenzelm # Date 1520085296 -3600 # Node ID 208235e594f64ac173cd3944b189ce382cc86f98 # Parent 197366313aafd6df5661472ef8a665ce31d7ea93 more operations; diff -r 197366313aaf -r 208235e594f6 src/Pure/General/mercurial.scala --- a/src/Pure/General/mercurial.scala Sat Mar 03 14:27:33 2018 +0100 +++ b/src/Pure/General/mercurial.scala Sat Mar 03 14:54:56 2018 +0100 @@ -114,6 +114,8 @@ def log(rev: String = "", template: String = "", options: String = ""): String = hg.command("log", opt_rev(rev) + opt_template(template), options).check.out + def parent(): String = log(rev = "p1()", template = "{node|short}") + def push(remote: String = "", rev: String = "", force: Boolean = false, options: String = "") { hg.command("push", opt_rev(rev) + opt_flag("--force", force) + optional(remote), options).