equal
deleted
inserted
replaced
49 [ "$#" -ne 0 ] && usage |
49 [ "$#" -ne 0 ] && usage |
50 |
50 |
51 |
51 |
52 ## main |
52 ## main |
53 |
53 |
54 #remove historic material |
|
55 rm -rf \ |
|
56 "$ISABELLE_HOME/lib/classes/Pure.jar" \ |
|
57 "$ISABELLE_HOME/lib/classes/Pure.shasum" \ |
|
58 "$ISABELLE_HOME/src/Tools/jEdit/dist" |
|
59 |
|
60 classpath "$CLASSPATH"; export CLASSPATH="" |
54 classpath "$CLASSPATH"; export CLASSPATH="" |
61 |
55 |
62 eval "declare -a JAVA_ARGS=($ISABELLE_TOOL_JAVA_OPTIONS)" |
56 eval "declare -a JAVA_ARGS=($ISABELLE_TOOL_JAVA_OPTIONS)" |
63 |
57 |
64 JAVA_ARGS["${#JAVA_ARGS[@]}"]="-classpath" |
58 JAVA_ARGS["${#JAVA_ARGS[@]}"]="-classpath" |