diff -r 18cbe1b8d859 -r 2e4d80723fb0 lib/Tools/install --- a/lib/Tools/install Sun Oct 02 15:35:56 2016 +0200 +++ b/lib/Tools/install Sun Oct 02 17:05:48 2016 +0200 @@ -63,7 +63,7 @@ mkdir -p "$BINDIR" || fail "Bad directory: \"$BINDIR\"" -for NAME in isabelle isabelle_scala_script +for NAME in isabelle isabelle_java isabelle_scala_script do BIN="$BINDIR/$NAME" DIST="$DISTDIR/bin/$NAME" @@ -74,4 +74,3 @@ echo "exec \"$DIST\" \"\$@\"" >> "$BIN" chmod +x "$BIN" done -