| changeset 74017 | b4e6b82fdb9e |
| parent 74011 | 1d366486a812 |
| child 74038 | b4f57bfe82e7 |
--- a/src/Tools/jEdit/lib/Tools/jedit Fri Jul 16 12:59:10 2021 +0200 +++ b/src/Tools/jEdit/lib/Tools/jedit Fri Jul 16 13:18:54 2021 +0200 @@ -155,9 +155,9 @@ ## main if [ -n "$FRESH_BUILD" ]; then - isabelle_admin_build jars_fresh || exit "$?" + isabelle_scala_build fresh || exit "$?" else - isabelle_admin_build jars || exit "$?" + isabelle_scala_build || exit "$?" fi if [ "$BUILD_ONLY" = false ]