equal
deleted
inserted
replaced
1 #!/usr/bin/env bash |
1 #!/usr/bin/env bash |
2 # |
2 # |
3 # Author: Makarius |
3 # Author: Makarius |
4 # |
4 # |
5 # DESCRIPTION: build Isabelle documentation |
5 # DESCRIPTION: build Isabelle documentation |
|
6 |
|
7 ## settings |
|
8 |
|
9 case "$ISABELLE_JAVA_PLATFORM" in |
|
10 x86-*) |
|
11 ISABELLE_BUILD_JAVA_OPTIONS="$ISABELLE_BUILD_JAVA_OPTIONS32" |
|
12 ;; |
|
13 x86_64-*) |
|
14 ISABELLE_BUILD_JAVA_OPTIONS="$ISABELLE_BUILD_JAVA_OPTIONS64" |
|
15 ;; |
|
16 esac |
6 |
17 |
7 |
18 |
8 ## diagnostics |
19 ## diagnostics |
9 |
20 |
10 PRG="$(basename "$0")" |
21 PRG="$(basename "$0")" |