lib/scripts/getsettings

--- a/lib/scripts/getsettings	Thu Sep 26 10:42:10 2013 +0200
+++ b/lib/scripts/getsettings	Thu Sep 26 12:56:59 2013 +0200
@@ -11,6 +11,11 @@
 
 ISABELLE_SETTINGS_PRESENT=true
 
+#GNU tar (notably on Mac OS X)
+if [ -x /usr/bin/gnutar ]; then
+  function tar() { /usr/bin/gnutar "$@"; }
+fi
+
 #Cygwin vs. POSIX
 if [ "$OSTYPE" = cygwin ]
 then