Admin/makebin
changeset 10097 1db5bd97f6a3
parent 10090 36d1218b58f4
child 10101 746263fbcbfd
equal deleted inserted replaced
10096:6cbe69107c18 10097:1db5bd97f6a3
    11 DISTBASE=~/tmp/isadist
    11 DISTBASE=~/tmp/isadist
    12 TMP="/tmp/isabelle-makebin$$"
    12 TMP="/tmp/isabelle-makebin$$"
    13 
    13 
    14 TAR=tar
    14 TAR=tar
    15 type -path gtar >/dev/null && TAR=gtar
    15 type -path gtar >/dev/null && TAR=gtar
       
    16 
       
    17 export THIS_IS_ISABELLE_BUILD=true
    16 
    18 
    17 
    19 
    18 ## diagnostics
    20 ## diagnostics
    19 
    21 
    20 PRG=$(basename "$0")
    22 PRG=$(basename "$0")