# 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 }