# HG changeset patch
# User wenzelm
# Date 1620125694 -7200
# Node ID f033d4f661e94aec6991fc929f446d68166a0989
# Parent  4b413b78cd948f063e597be95f3570f151c822e4
tuned signature;

diff -r 4b413b78cd94 -r f033d4f661e9 src/Pure/General/mercurial.scala
--- a/src/Pure/General/mercurial.scala	Sun May 02 21:46:59 2021 +0200
+++ b/src/Pure/General/mercurial.scala	Tue May 04 12:54:54 2021 +0200
@@ -78,8 +78,8 @@
         val content = download_archive(rev = rev, progress = progress)
         Bytes.write(archive_path, content.bytes)
         progress.echo("Unpacking " + rev + ".tar.gz")
-        Isabelle_System.gnutar("-xzf " + File.bash_path(archive_path) + " --strip-components=1",
-          dir = dir, original_owner = true).check
+        Isabelle_System.gnutar("-xzf " + File.bash_path(archive_path),
+          dir = dir, original_owner = true, strip = 1).check
       })
     }
   }
diff -r 4b413b78cd94 -r f033d4f661e9 src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Sun May 02 21:46:59 2021 +0200
+++ b/src/Pure/System/isabelle_system.scala	Tue May 04 12:54:54 2021 +0200
@@ -531,11 +531,13 @@
     args: String,
     dir: Path = Path.current,
     original_owner: Boolean = false,
+    strip: Int = 0,
     redirect: Boolean = false): Process_Result =
   {
     val options =
       (if (dir.is_current) "" else "-C " + File.bash_path(dir) + " ") +
-      (if (original_owner) "" else "--owner=root --group=staff ")
+      (if (original_owner) "" else "--owner=root --group=staff ") +
+      (if (strip <= 0) "" else "--strip-components=" + strip + " ")
 
     if (gnutar_check) bash("tar " + options + args, redirect = redirect)
     else error("Expected to find GNU tar executable")