lib/Tools/java
changeset 67490 982f0bf34804
parent 66906 03a96b8c7c06
child 69126 e1b4b14ded58
equal deleted inserted replaced
67488:3d33847dc911 67490:982f0bf34804
     8 
     8 
     9 [ -n "$CLASSPATH" ] && classpath "$CLASSPATH"
     9 [ -n "$CLASSPATH" ] && classpath "$CLASSPATH"
    10 unset CLASSPATH
    10 unset CLASSPATH
    11 
    11 
    12 isabelle_java java "${JAVA_ARGS[@]}" \
    12 isabelle_java java "${JAVA_ARGS[@]}" \
       
    13   "-Djava.ext.dirs=$(platform_path "$ISABELLE_JDK_HOME/jre/lib/ext")" \
    13   -classpath "$(platform_path "$ISABELLE_CLASSPATH")" "$@"
    14   -classpath "$(platform_path "$ISABELLE_CLASSPATH")" "$@"