# HG changeset patch
# User wenzelm
# Date 1475504159 -7200
# Node ID 355b78441650f30389d19b2189a229678698f9c0
# Parent  f6e965cf1617d3a92fdd2a6d9e4fc0e8450dca3a
clarified: a variant of -i is the default, but its output is not as precise as it might seem;

diff -r f6e965cf1617 -r 355b78441650 src/Pure/General/mercurial.scala
--- 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