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