lib/Tools/java
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