prefer GNU tar for Isabelle to avoid odd extended header keywords produced by Apple's bsdtar (see also 8f6046b7f850);
authorwenzelm
Thu Sep 26 12:56:59 2013 +0200 (2013-09-26)
changeset 539135ff12177a067
parent 53912 f6fb8ca4517f
child 53914 48072f049838
prefer GNU tar for Isabelle to avoid odd extended header keywords produced by Apple's bsdtar (see also 8f6046b7f850);
Admin/Release/build_library
Admin/java/build
Admin/lib/Tools/makedist
Admin/lib/Tools/makedist_bundle
lib/scripts/getsettings
     1.1 --- a/Admin/Release/build_library	Thu Sep 26 10:42:10 2013 +0200
     1.2 +++ b/Admin/Release/build_library	Thu Sep 26 12:56:59 2013 +0200
     1.3 @@ -61,7 +61,10 @@
     1.4  
     1.5  ## main
     1.6  
     1.7 -export COPYFILE_DISABLE=true
     1.8 +#GNU tar (notably on Mac OS X)
     1.9 +if [ -x /usr/bin/gnutar ]; then
    1.10 +  function tar() { /usr/bin/gnutar "$@"; }
    1.11 +fi
    1.12  
    1.13  TMP="/var/tmp/isabelle-makedist$$"
    1.14  mkdir "$TMP" || fail "Cannot create directory: \"$TMP\""
     2.1 --- a/Admin/java/build	Thu Sep 26 10:42:10 2013 +0200
     2.2 +++ b/Admin/java/build	Thu Sep 26 12:56:59 2013 +0200
     2.3 @@ -71,7 +71,10 @@
     2.4  
     2.5  # content
     2.6  
     2.7 -export COPYFILE_DISABLE=true
     2.8 +#GNU tar (notably on Mac OS X)
     2.9 +if [ -x /usr/bin/gnutar ]; then
    2.10 +  function tar() { /usr/bin/gnutar "$@"; }
    2.11 +fi
    2.12  
    2.13  mkdir "$DIR/x86-linux" "$DIR/x86_64-linux" "$DIR/x86_64-darwin" "$DIR/x86-cygwin"
    2.14  
     3.1 --- a/Admin/lib/Tools/makedist	Thu Sep 26 10:42:10 2013 +0200
     3.2 +++ b/Admin/lib/Tools/makedist	Thu Sep 26 12:56:59 2013 +0200
     3.3 @@ -199,7 +199,7 @@
     3.4  chmod -R g=o "$DISTNAME"
     3.5  
     3.6  echo "$DISTBASE/$DISTNAME.tar.gz"
     3.7 -env COPYFILE_DISABLE=true tar -c -z -f "$DISTNAME.tar.gz" "$DISTNAME"
     3.8 +tar -c -z -f "$DISTNAME.tar.gz" "$DISTNAME"
     3.9  [ "$?" = 0 ] || exit "$?"
    3.10  
    3.11  
     4.1 --- a/Admin/lib/Tools/makedist_bundle	Thu Sep 26 10:42:10 2013 +0200
     4.2 +++ b/Admin/lib/Tools/makedist_bundle	Thu Sep 26 12:56:59 2013 +0200
     4.3 @@ -41,8 +41,6 @@
     4.4  
     4.5  ## main
     4.6  
     4.7 -export COPYFILE_DISABLE=true
     4.8 -
     4.9  TMP="/var/tmp/isabelle-makedist$$"
    4.10  mkdir "$TMP" || fail "Cannot create directory $TMP"
    4.11  
     5.1 --- a/lib/scripts/getsettings	Thu Sep 26 10:42:10 2013 +0200
     5.2 +++ b/lib/scripts/getsettings	Thu Sep 26 12:56:59 2013 +0200
     5.3 @@ -11,6 +11,11 @@
     5.4  
     5.5  ISABELLE_SETTINGS_PRESENT=true
     5.6  
     5.7 +#GNU tar (notably on Mac OS X)
     5.8 +if [ -x /usr/bin/gnutar ]; then
     5.9 +  function tar() { /usr/bin/gnutar "$@"; }
    5.10 +fi
    5.11 +
    5.12  #Cygwin vs. POSIX
    5.13  if [ "$OSTYPE" = cygwin ]
    5.14  then