# HG changeset patch
# User wenzelm
# Date 1317732711 -7200
# Node ID 21c09b727bf35de8e4d758869a65bada082f7ff3
# Parent  0a3f301271ba3146dbcb3f8b09debca34653cb37
more explicit check of Java executable -- relevant for Linux x86/x86_64 mismatch and absence on Mac OS Lion;

diff -r 0a3f301271ba -r 21c09b727bf3 lib/Tools/java
--- 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