src/Pure/General/mercurial.scala
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