changeset 73705 | ac07f6be27ea |
parent 73192 | e7437085e589 |
73704:7c7a59b76528 | 73705:ac07f6be27ea |
---|---|
1 #!/usr/bin/env bash |
1 #!/usr/bin/env bash |
2 |
2 |
3 set -e |
3 set -e |
4 |
4 |
5 unset CDPATH |
|
5 THIS="$(cd "$(dirname "$0")"; pwd)" |
6 THIS="$(cd "$(dirname "$0")"; pwd)" |
6 cd "$THIS" |
7 cd "$THIS" |
7 |
8 |
8 source "../../lib/scripts/isabelle-platform" |
9 source "../../lib/scripts/isabelle-platform" |
9 |
10 |