src/Pure/General/mercurial.scala

--- a/src/Pure/General/mercurial.scala	Sat Nov 12 17:00:26 2016 +0100
+++ b/src/Pure/General/mercurial.scala	Sat Nov 12 17:58:11 2016 +0100
@@ -92,6 +92,9 @@
       }
     }
 
+    def archive(target: String, rev: String = "", options: String = ""): Unit =
+      hg.command("archive", opt_rev(rev) + " " + Bash.string(target), options).check
+
     def heads(template: String = "{node|short}\n", options: String = ""): List[String] =
       hg.command("heads", opt_template(template), options).check.out_lines