--- 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")