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