lib/scripts/getsettings
changeset 53913 5ff12177a067
parent 53580 ffc926553ec5
child 53967 bfaae48b0ce0
     1.1 --- a/lib/scripts/getsettings	Thu Sep 26 10:42:10 2013 +0200
     1.2 +++ b/lib/scripts/getsettings	Thu Sep 26 12:56:59 2013 +0200
     1.3 @@ -11,6 +11,11 @@
     1.4  
     1.5  ISABELLE_SETTINGS_PRESENT=true
     1.6  
     1.7 +#GNU tar (notably on Mac OS X)
     1.8 +if [ -x /usr/bin/gnutar ]; then
     1.9 +  function tar() { /usr/bin/gnutar "$@"; }
    1.10 +fi
    1.11 +
    1.12  #Cygwin vs. POSIX
    1.13  if [ "$OSTYPE" = cygwin ]
    1.14  then