# HG changeset patch
# User wenzelm
# Date 1653769991 -7200
# Node ID e3f753ef0b5c95fd6397a43094d131b8e37ef170
# Parent  c2fb64822a7b9a3d55060b03a813aad397620dab
tuned signature;

diff -r c2fb64822a7b -r e3f753ef0b5c src/Pure/General/mercurial.scala
--- a/src/Pure/General/mercurial.scala	Sat May 28 22:33:04 2022 +0200
+++ b/src/Pure/General/mercurial.scala	Sat May 28 22:33:11 2022 +0200
@@ -238,8 +238,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").check.out_lines
+    def status(options: String = ""): List[String] =
+      hg.command("status", options = options).check.out_lines
+
+    def known_files(): List[String] = status(options = "--modified --added --clean --no-status")
 
     def graph(): Graph = {
       val Node = """^node: (\w{12}) (\w{12}) (\w{12})""".r