# HG changeset patch
# User wenzelm
# Date 1475431617 -7200
# Node ID 2f38d8aff2f5ff994ef59b4858ec4cea0dbc1184
# Parent  e11ccb5aa82f93a8c7547a9fcfe5e282cd0c7711
more operations;

diff -r e11ccb5aa82f -r 2f38d8aff2f5 src/Pure/General/mercurial.scala
--- a/src/Pure/General/mercurial.scala	Sun Oct 02 19:47:18 2016 +0200
+++ b/src/Pure/General/mercurial.scala	Sun Oct 02 20:06:57 2016 +0200
@@ -30,8 +30,11 @@
     def command(cmd: String, cwd: JFile = null): Process_Result =
       Isabelle_System.hg("--repository " + File.bash_path(root) + " " + cmd, cwd = cwd)
 
-    def manifest(rev: String = "", cwd: JFile = null): List[String] =
-      command("manifest" + opt_rev(rev), cwd = cwd).check.out_lines
+    def identify(rev: String = "", options: String = ""): String =
+      command("id -i " + 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
 
     command("root").check
   }