Admin/build
changeset 43521 d477b92109b8
parent 43280 e5dd0ae1b054
child 45091 bf56eb7af632
equal deleted inserted replaced
43520:cec9b95fa35d 43521:d477b92109b8
    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   pushd "$ISABELLE_HOME/src/Pure" >/dev/null
    88   pushd "$ISABELLE_HOME/src/Pure" >/dev/null
    88   "$ISABELLE_TOOL" env ./build-jars "$@" || exit $?
    89   "$ISABELLE_TOOL" env ./build-jars "$@" || exit $?
    89   popd >/dev/null
    90   popd >/dev/null
    90 }
    91 }
    91 
    92