omit pointless option;
authorwenzelm
Sun, 29 May 2022 17:37:43 +0200
changeset 75478 904607aedc4b
parent 75477 1f0016095195
child 75479 4363ad65ad36
omit pointless option;
src/Pure/Admin/build_release.scala
--- a/src/Pure/Admin/build_release.scala	Sun May 29 17:26:38 2022 +0200
+++ b/src/Pure/Admin/build_release.scala	Sun May 29 17:37:43 2022 +0200
@@ -412,7 +412,7 @@
 
       Isabelle_System.new_directory(context.dist_dir)
 
-      hg.archive(context.isabelle_dir.expand.implode, rev = id, options = "--type files")
+      hg.archive(context.isabelle_dir.expand.implode, rev = id)
 
       for (name <- List(".hg_archival.txt", ".hgtags", ".hgignore", "README_REPOSITORY")) {
         (context.isabelle_dir + Path.explode(name)).file.delete