src/Pure/General/mercurial.scala
changeset 75824 a2b2e8964e1a
parent 75559 5340239ff468
child 76131 8b695e59db3f
--- a/src/Pure/General/mercurial.scala	Fri Aug 12 15:57:22 2022 +0200
+++ b/src/Pure/General/mercurial.scala	Fri Aug 12 16:01:52 2022 +0200
@@ -323,10 +323,10 @@
 
         Rsync.init(context0, target,
           contents =
-            File.Content(Hg_Sync.PATH_ID, id_content) ::
-            File.Content(Hg_Sync.PATH_LOG, log_content) ::
-            File.Content(Hg_Sync.PATH_DIFF, diff_content) ::
-            File.Content(Hg_Sync.PATH_STAT, stat_content) :: contents)
+            File.content(Hg_Sync.PATH_ID, id_content) ::
+            File.content(Hg_Sync.PATH_LOG, log_content) ::
+            File.content(Hg_Sync.PATH_DIFF, diff_content) ::
+            File.content(Hg_Sync.PATH_STAT, stat_content) :: contents)
 
         val (exclude, source) =
           if (rev.isEmpty) {