changeset 65822 | 17b8528c2f53 |
parent 65819 | ff3dc9325eaa |
child 65825 | 11f87ab51ddb |
--- a/src/Pure/General/mercurial.scala Sun May 14 15:16:38 2017 +0200 +++ b/src/Pure/General/mercurial.scala Sun May 14 15:34:20 2017 +0200 @@ -138,6 +138,10 @@ opt_rev(rev) + opt_flag("--clean", clean) + opt_flag("--check", check), options).check } + def known_files(): List[String] = + hg.command("status", options = "--modified --added --clean --no-status --color=never"). + check.out_lines + def length(): Int = identify(options = "-n") match { case Value.Int(n) => n + 1