--- a/src/Pure/General/mercurial.scala Mon Oct 03 12:39:03 2016 +0200
+++ b/src/Pure/General/mercurial.scala Mon Oct 03 16:15:59 2016 +0200
@@ -40,7 +40,7 @@
command("heads " + options + opt_template(template)).check.out_lines
def identify(rev: String = "", options: String = ""): String =
- command("id -i " + options + opt_rev(rev)).check.out_lines.headOption getOrElse ""
+ command("id " + options + opt_rev(rev)).check.out_lines.headOption getOrElse ""
def manifest(rev: String = "", options: String = ""): List[String] =
command("manifest " + options + opt_rev(rev)).check.out_lines