changeset 63897 | 85c83757788c |
parent 63490 | 9416333a17c2 |
child 64144 | ef20d2da71af |
--- 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"