changeset 15971 | c0c4088edccf |
parent 14633 | 8553a957cffa |
child 17571 | 5f83a635dce0 |
15970:b8855873d234 | 15971:c0c4088edccf |
---|---|
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 |
|
18 |
17 |
19 |
18 |
20 ## diagnostics |
19 ## diagnostics |
21 |
20 |
22 PRG=$(basename "$0") |
21 PRG=$(basename "$0") |