# HG changeset patch
# User wenzelm
# Date 1380193019 -7200
# Node ID 5ff12177a067865b77ca0b6223543e462e67467f
# Parent  f6fb8ca4517fa91552840daed75a873f55d7456f
prefer GNU tar for Isabelle to avoid odd extended header keywords produced by Apple's bsdtar (see also 8f6046b7f850);

diff -r f6fb8ca4517f -r 5ff12177a067 Admin/Release/build_library
--- a/Admin/Release/build_library	Thu Sep 26 10:42:10 2013 +0200
+++ b/Admin/Release/build_library	Thu Sep 26 12:56:59 2013 +0200
@@ -61,7 +61,10 @@
 
 ## main
 
-export COPYFILE_DISABLE=true
+#GNU tar (notably on Mac OS X)
+if [ -x /usr/bin/gnutar ]; then
+  function tar() { /usr/bin/gnutar "$@"; }
+fi
 
 TMP="/var/tmp/isabelle-makedist$$"
 mkdir "$TMP" || fail "Cannot create directory: \"$TMP\""
diff -r f6fb8ca4517f -r 5ff12177a067 Admin/java/build
--- a/Admin/java/build	Thu Sep 26 10:42:10 2013 +0200
+++ b/Admin/java/build	Thu Sep 26 12:56:59 2013 +0200
@@ -71,7 +71,10 @@
 
 # content
 
-export COPYFILE_DISABLE=true
+#GNU tar (notably on Mac OS X)
+if [ -x /usr/bin/gnutar ]; then
+  function tar() { /usr/bin/gnutar "$@"; }
+fi
 
 mkdir "$DIR/x86-linux" "$DIR/x86_64-linux" "$DIR/x86_64-darwin" "$DIR/x86-cygwin"
 
diff -r f6fb8ca4517f -r 5ff12177a067 Admin/lib/Tools/makedist
--- a/Admin/lib/Tools/makedist	Thu Sep 26 10:42:10 2013 +0200
+++ b/Admin/lib/Tools/makedist	Thu Sep 26 12:56:59 2013 +0200
@@ -199,7 +199,7 @@
 chmod -R g=o "$DISTNAME"
 
 echo "$DISTBASE/$DISTNAME.tar.gz"
-env COPYFILE_DISABLE=true tar -c -z -f "$DISTNAME.tar.gz" "$DISTNAME"
+tar -c -z -f "$DISTNAME.tar.gz" "$DISTNAME"
 [ "$?" = 0 ] || exit "$?"
 
 
diff -r f6fb8ca4517f -r 5ff12177a067 Admin/lib/Tools/makedist_bundle
--- a/Admin/lib/Tools/makedist_bundle	Thu Sep 26 10:42:10 2013 +0200
+++ b/Admin/lib/Tools/makedist_bundle	Thu Sep 26 12:56:59 2013 +0200
@@ -41,8 +41,6 @@
 
 ## main
 
-export COPYFILE_DISABLE=true
-
 TMP="/var/tmp/isabelle-makedist$$"
 mkdir "$TMP" || fail "Cannot create directory $TMP"
 
diff -r f6fb8ca4517f -r 5ff12177a067 lib/scripts/getsettings
--- a/lib/scripts/getsettings	Thu Sep 26 10:42:10 2013 +0200
+++ b/lib/scripts/getsettings	Thu Sep 26 12:56:59 2013 +0200
@@ -11,6 +11,11 @@
 
 ISABELLE_SETTINGS_PRESENT=true
 
+#GNU tar (notably on Mac OS X)
+if [ -x /usr/bin/gnutar ]; then
+  function tar() { /usr/bin/gnutar "$@"; }
+fi
+
 #Cygwin vs. POSIX
 if [ "$OSTYPE" = cygwin ]
 then