author | wenzelm |
Tue, 04 Oct 2011 14:51:51 +0200 | |
changeset 45105 | 21c09b727bf3 |
parent 45104 | 0a3f301271ba |
child 45106 | 3498077f2012 |
lib/Tools/java | file | annotate | diff | comparison | revisions |
--- a/lib/Tools/java Mon Oct 03 11:16:51 2011 +0200 +++ b/lib/Tools/java Tue Oct 04 14:51:51 2011 +0200 @@ -8,6 +8,13 @@ JAVA_EXE="${THIS_JAVA:-$ISABELLE_JAVA}" +if "$JAVA_EXE" -version >/dev/null 2>/dev/null; then + : +else + echo "Bad Java executable: \"$JAVA_EXE\"" >&2 + exit 2 +fi + if "$JAVA_EXE" -server >/dev/null 2>/dev/null; then SERVER="-server" else