changeset 12427 | 37cfec8dfe8e |
parent 11576 | c418146c4763 |
child 12721 | 226fc0e2e7e3 |
12426:9032bdbc2125 | 12427:37cfec8dfe8e |
---|---|
7 |
7 |
8 ## global settings |
8 ## global settings |
9 |
9 |
10 FAKE_BUILD="" |
10 FAKE_BUILD="" |
11 DISTBASE=~/tmp/isadist |
11 DISTBASE=~/tmp/isadist |
12 TMP="/tmp/isabelle-makebin$$" |
12 TMP="/var/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 |
16 |
17 export THIS_IS_ISABELLE_BUILD=true |
17 export THIS_IS_ISABELLE_BUILD=true |