equal
deleted
inserted
replaced
49 shift $(($OPTIND - 1)) |
49 shift $(($OPTIND - 1)) |
50 |
50 |
51 |
51 |
52 ## main |
52 ## main |
53 |
53 |
54 [ -e "$ISABELLE_HOME/Admin/build" ] && { "$ISABELLE_HOME/Admin/build" jars || exit $?; } |
54 isabelle_admin_build jars || exit $? |
55 |
55 |
56 declare -a JAVA_ARGS; eval "JAVA_ARGS=($ISABELLE_BUILD_JAVA_OPTIONS)" |
56 declare -a JAVA_ARGS; eval "JAVA_ARGS=($ISABELLE_BUILD_JAVA_OPTIONS)" |
57 |
57 |
58 "$ISABELLE_TOOL" java "${JAVA_ARGS[@]}" isabelle.Keywords keywords \ |
58 "$ISABELLE_TOOL" java "${JAVA_ARGS[@]}" isabelle.Keywords keywords \ |
59 "$KEYWORDS_NAME" "${DIRS[@]}" $'\n' "$@" |
59 "$KEYWORDS_NAME" "${DIRS[@]}" $'\n' "$@" |