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: Isabelle/jEdit interface wrapper |
5 # DESCRIPTION: Isabelle/jEdit interface wrapper |
6 |
|
7 |
|
8 ## settings |
|
9 |
|
10 case "$ISABELLE_JAVA_PLATFORM" in |
|
11 x86_64-*) |
|
12 JEDIT_JAVA_OPTIONS="$JEDIT_JAVA_OPTIONS64" |
|
13 ;; |
|
14 *) |
|
15 JEDIT_JAVA_OPTIONS="$JEDIT_JAVA_OPTIONS32" |
|
16 ;; |
|
17 esac |
|
18 |
6 |
19 |
7 |
20 ## sources |
8 ## sources |
21 |
9 |
22 declare -a SOURCES_BASE=( |
10 declare -a SOURCES_BASE=( |
210 ;; |
198 ;; |
211 esac |
199 esac |
212 done |
200 done |
213 } |
201 } |
214 |
202 |
215 declare -a JAVA_ARGS; eval "JAVA_ARGS=($JEDIT_JAVA_SYSTEM_OPTIONS $JEDIT_JAVA_OPTIONS)" |
203 eval "declare -a JAVA_ARGS=($JEDIT_JAVA_SYSTEM_OPTIONS $JEDIT_JAVA_OPTIONS)" |
216 |
204 |
217 declare -a ARGS=() |
205 declare -a ARGS=() |
218 |
206 |
219 declare -a OPTIONS; eval "OPTIONS=($ISABELLE_JEDIT_OPTIONS)" |
207 declare -a OPTIONS; eval "OPTIONS=($ISABELLE_JEDIT_OPTIONS)" |
220 getoptions "${OPTIONS[@]}" |
208 getoptions "${OPTIONS[@]}" |