--- a/Admin/Release/CHECKLIST Fri Sep 16 17:37:41 2016 +0200
+++ b/Admin/Release/CHECKLIST Fri Sep 16 18:01:31 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)
--- a/Admin/Release/build_library Fri Sep 16 17:37:41 2016 +0200
+++ b/Admin/Release/build_library Fri Sep 16 18:01:31 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\""
--- a/Admin/java/build Fri Sep 16 17:37:41 2016 +0200
+++ b/Admin/java/build Fri Sep 16 18:01:31 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"
--- a/Admin/lib/Tools/makedist Fri Sep 16 17:37:41 2016 +0200
+++ b/Admin/lib/Tools/makedist Fri Sep 16 18:01:31 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"
--- a/Admin/lib/Tools/makedist_bundle Fri Sep 16 17:37:41 2016 +0200
+++ b/Admin/lib/Tools/makedist_bundle Fri Sep 16 18:01:31 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"