# HG changeset patch
# User wenzelm
# Date 1654536482 -7200
# Node ID 931c48756b88ee14697a47c40d52b9e9b19b6f26
# Parent  cb4af8c6152f35e9a4c32924f39709633f17adb1
avoid redundant meta data: exclude .hg_archival.txt;

diff -r cb4af8c6152f -r 931c48756b88 src/Pure/General/mercurial.scala
--- a/src/Pure/General/mercurial.scala	Mon Jun 06 19:19:12 2022 +0200
+++ b/src/Pure/General/mercurial.scala	Mon Jun 06 19:28:02 2022 +0200
@@ -329,22 +329,22 @@
             File.Content(Hg_Sync.PATH_DIFF, diff_content) ::
             File.Content(Hg_Sync.PATH_STAT, stat_content) :: contents)
 
-        val (options, source) =
+        val (exclude, source) =
           if (rev.isEmpty) {
-            val exclude_path = tmp_dir + Path.explode("exclude")
-            val exclude = status(options = "--unknown --ignored --no-status")
-            File.write(exclude_path, cat_lines((".hg" :: exclude).map("/" + _)))
-
-            val options = List("--exclude-from=" + exclude_path.implode)
+            val exclude = ".hg" :: status(options = "--unknown --ignored --no-status")
             val source = File.standard_path(root)
-            (options, source)
+            (exclude, source)
           }
           else {
+            val exclude = List(".hg_archival.txt")
             val source = File.standard_path(tmp_dir + Path.explode("archive"))
             archive(source, rev = rev)
-            (Nil, source)
+            (exclude, source)
           }
 
+        val exclude_path = tmp_dir + Path.explode("exclude")
+        File.write(exclude_path, cat_lines(exclude.map("/" + _)))
+
         val protect =
           (Hg_Sync.PATH :: contents.map(_.path))
             .map(path => "protect /" + File.standard_path(path))
@@ -354,7 +354,8 @@
           clean = true,
           prune_empty_dirs = true,
           filter = protect ::: filter,
-          args = options ::: List("--", Isabelle_System.rsync_dir(source), target)
+          args = List("--exclude-from=" + exclude_path.implode, "--",
+            Isabelle_System.rsync_dir(source), target)
         ).check
       }
     }