diff -r 3e72fab0e699 -r b81b2c50fc7c src/Pure/General/mercurial.scala
--- a/src/Pure/General/mercurial.scala	Sat Apr 08 19:02:51 2023 +0200
+++ b/src/Pure/General/mercurial.scala	Sat Apr 08 19:32:09 2023 +0200
@@ -552,7 +552,6 @@
     Isabelle_Tool("hg_sync", "synchronize Mercurial repository with target directory",
       Scala_Project.here, { args =>
         var filter: List[String] = Nil
-        var protect_args = false
         var root: Option[Path] = None
         var thorough = false
         var dry_run = false
@@ -569,7 +568,6 @@
   Options are:
     -F RULE      add rsync filter RULE
                  (e.g. "protect /foo" to avoid deletion)
-    -P           protect spaces in target file names: more robust, less portable
     -R ROOT      explicit repository root directory
                  (default: implicit from current directory)
     -T           thorough treatment of file content and directory times
@@ -585,7 +583,6 @@
   which can be local or remote (see options -s -p -u).
 """,
           "F:" -> (arg => filter = filter ::: List(arg)),
-          "P" -> (_ => protect_args = true),
           "R:" -> (arg => root = Some(Path.explode(arg))),
           "T" -> (_ => thorough = true),
           "n" -> (_ => dry_run = true),
@@ -611,7 +608,7 @@
           }
 
         using(SSH.open_system(options, host = ssh_host, port = ssh_port, user = ssh_user)) { ssh =>
-          val context = Rsync.Context(progress = progress, ssh = ssh, protect_args = protect_args)
+          val context = Rsync.Context(progress = progress, ssh = ssh)
           hg.sync(context, target, thorough = thorough, dry_run = dry_run,
             filter = filter, rev = rev)
         }