# HG changeset patch
# User wenzelm
# Date 1474038759 -7200
# Node ID 85c83757788c431d59bd6e0b7a39d514c32a5294
# Parent  3dd6bde2502d5969ab6f54d399e016ec2ed4a64f
consolidate implicit use of gnutar, via somewhat fragile dynamic scoping within existing shell scripts;

diff -r 3dd6bde2502d -r 85c83757788c Admin/Release/CHECKLIST
--- a/Admin/Release/CHECKLIST	Fri Sep 16 16:15:11 2016 +0200
+++ b/Admin/Release/CHECKLIST	Fri Sep 16 17:12:39 2016 +0200
@@ -69,11 +69,14 @@
 Packaging
 =========
 
+- Mac OS X: provide "gnutar" executable via shell PATH
+  (e.g. copy of /usr/bin/gnutar from Mountain Lion)
+
 - fully-automated packaging:
 
   hg up -r DISTNAME && Admin/Release/build -O -l -r DISTNAME /home/isabelle/dist
 
-  Mac OS X: requires gnutar, avoid Mavericks (problems with hdiutil?)
+  Mac OS X: avoid Mavericks (problems with hdiutil?)
   Linux: avoid Debian (bitmap fonts for prog-prove)
 
 
diff -r 3dd6bde2502d -r 85c83757788c Admin/Release/build_library
--- a/Admin/Release/build_library	Fri Sep 16 16:15:11 2016 +0200
+++ b/Admin/Release/build_library	Fri Sep 16 17:12:39 2016 +0200
@@ -62,9 +62,7 @@
 ## main
 
 #GNU tar (notably on Mac OS X)
-if [ -x /usr/bin/gnutar ]; then
-  function tar() { /usr/bin/gnutar "$@"; }
-fi
+type -p gnutar >/dev/null && function tar() { gnutar "$@"; }
 
 TMP="/var/tmp/isabelle-makedist$$"
 mkdir "$TMP" || fail "Cannot create directory: \"$TMP\""
diff -r 3dd6bde2502d -r 85c83757788c Admin/java/build
--- a/Admin/java/build	Fri Sep 16 16:15:11 2016 +0200
+++ b/Admin/java/build	Fri Sep 16 17:12:39 2016 +0200
@@ -53,9 +53,7 @@
 # content
 
 #GNU tar (notably on Mac OS X)
-if [ -x /usr/bin/gnutar ]; then
-  function tar() { /usr/bin/gnutar "$@"; }
-fi
+type -p gnutar >/dev/null && function tar() { gnutar "$@"; }
 
 mkdir "$DIR/x86-linux" "$DIR/x86_64-linux" "$DIR/x86-windows" "$DIR/x86_64-windows" "$DIR/x86_64-darwin"
 
diff -r 3dd6bde2502d -r 85c83757788c Admin/lib/Tools/makedist
--- a/Admin/lib/Tools/makedist	Fri Sep 16 16:15:11 2016 +0200
+++ b/Admin/lib/Tools/makedist	Fri Sep 16 17:12:39 2016 +0200
@@ -202,6 +202,9 @@
 
 # create archive
 
+#GNU tar (notably on Mac OS X)
+type -p gnutar >/dev/null && function tar() { gnutar "$@"; }
+
 echo "### Creating archive"
 
 cd "$DISTBASE"
diff -r 3dd6bde2502d -r 85c83757788c Admin/lib/Tools/makedist_bundle
--- a/Admin/lib/Tools/makedist_bundle	Fri Sep 16 16:15:11 2016 +0200
+++ b/Admin/lib/Tools/makedist_bundle	Fri Sep 16 17:12:39 2016 +0200
@@ -47,6 +47,9 @@
 
 ## main
 
+#GNU tar (notably on Mac OS X)
+type -p gnutar >/dev/null && function tar() { gnutar "$@"; }
+
 TMP="/var/tmp/isabelle-makedist$$"
 mkdir "$TMP" || fail "Cannot create directory $TMP"