Admin/build
changeset 45091 bf56eb7af632
parent 43521 d477b92109b8
child 45385 7c1375ba1424
equal deleted inserted replaced
45090:e392d0a28bd8 45091:bf56eb7af632
    82 }
    82 }
    83 
    83 
    84 
    84 
    85 function build_jars ()
    85 function build_jars ()
    86 {
    86 {
    87   "$ISABELLE_HOME/lib/scripts/java_ext_dirs" >/dev/null
    87   "$ISABELLE_TOOL" env "$ISABELLE_HOME/lib/scripts/java_ext_dirs" >/dev/null
    88   pushd "$ISABELLE_HOME/src/Pure" >/dev/null
    88   pushd "$ISABELLE_HOME/src/Pure" >/dev/null
    89   "$ISABELLE_TOOL" env ./build-jars "$@" || exit $?
    89   "$ISABELLE_TOOL" env ./build-jars "$@" || exit $?
    90   popd >/dev/null
    90   popd >/dev/null
    91 }
    91 }
    92 
    92