equal
deleted
inserted
replaced
126 shift $(($OPTIND - 1)) |
126 shift $(($OPTIND - 1)) |
127 |
127 |
128 |
128 |
129 ## main |
129 ## main |
130 |
130 |
131 [ -e "$ISABELLE_HOME/Admin/build" ] && { "$ISABELLE_HOME/Admin/build" jars || exit $?; } |
131 isabelle_admin_build jars || exit $? |
132 |
132 |
133 if [ "$NO_BUILD" = false -a "$VERBOSE" = true ]; then |
133 if [ "$NO_BUILD" = false -a "$VERBOSE" = true ]; then |
134 echo "Started at $(date) ($ML_IDENTIFIER on $(hostname))" |
134 echo "Started at $(date) ($ML_IDENTIFIER on $(hostname))" |
135 |
135 |
136 show_settings "" |
136 show_settings "" |