changeset 45990 | 21c09b727bf3 |
parent 44401 | d477b92109b8 |
child 46258 | 7c1375ba1424 |
1.1 --- a/lib/Tools/java Mon Oct 03 11:16:51 2011 +0200 1.2 +++ b/lib/Tools/java Tue Oct 04 14:51:51 2011 +0200 1.3 @@ -8,6 +8,13 @@ 1.4 1.5 JAVA_EXE="${THIS_JAVA:-$ISABELLE_JAVA}" 1.6 1.7 +if "$JAVA_EXE" -version >/dev/null 2>/dev/null; then 1.8 + : 1.9 +else 1.10 + echo "Bad Java executable: \"$JAVA_EXE\"" >&2 1.11 + exit 2 1.12 +fi 1.13 + 1.14 if "$JAVA_EXE" -server >/dev/null 2>/dev/null; then 1.15 SERVER="-server" 1.16 else