changeset 12985 | 9db054a40247 |
parent 12830 | c037ff3e5ddf |
child 13001 | 40ba2eee948e |
12984:6071200efbf6 | 12985:9db054a40247 |
---|---|
12 |
12 |
13 TAR=tar |
13 TAR=tar |
14 type -path gtar >/dev/null && TAR=gtar |
14 type -path gtar >/dev/null && TAR=gtar |
15 |
15 |
16 export THIS_IS_ISABELLE_BUILD=true |
16 export THIS_IS_ISABELLE_BUILD=true |
17 export THIS_IS_ISABELLE_ADMIN=true |
|
17 |
18 |
18 |
19 |
19 ## diagnostics |
20 ## diagnostics |
20 |
21 |
21 PRG=$(basename "$0") |
22 PRG=$(basename "$0") |