more robust: no change of directory attributes of initial test, notably target without .hg_sync meta data;
authorwenzelm
Tue, 07 Jun 2022 17:47:28 +0200
changeset 75534 1d937b12204d
parent 75529 31abccc97ade
child 75535 2bf2cc3aca84
more robust: no change of directory attributes of initial test, notably target without .hg_sync meta data;
src/Pure/General/rsync.scala
--- a/src/Pure/General/rsync.scala	Tue Jun 07 17:24:42 2022 +0200
+++ b/src/Pure/General/rsync.scala	Tue Jun 07 17:47:28 2022 +0200
@@ -49,8 +49,11 @@
     Isabelle_System.with_tmp_dir("sync") { tmp_dir =>
       val init_dir = Isabelle_System.make_directory(tmp_dir + Path.explode("init"))
       contents.foreach(_.write(init_dir))
-      exec(context, thorough = true,
-        args = List(File.bash_path(init_dir) + "/.", target)).check
+      exec(context.copy(archive = false),
+        thorough = true,
+        args =
+          List(if (contents.nonEmpty) "--archive" else "--dirs",
+            File.bash_path(init_dir) + "/.", target)).check
     }
 
   def terminate(target: String): String =