lib/scripts/java_ext_dirs
changeset 43521 d477b92109b8
parent 43518 7cad71ca9bcc
child 43522 2562d6c81b03
equal deleted inserted replaced
43520:cec9b95fa35d 43521:d477b92109b8
    34 
    34 
    35 
    35 
    36 ## main
    36 ## main
    37 
    37 
    38 JAVA_EXE="${THIS_JAVA:-$ISABELLE_JAVA}"
    38 JAVA_EXE="${THIS_JAVA:-$ISABELLE_JAVA}"
    39 exec "$JAVA_EXE" -classpath "$(jvmpath "$TARGET")" isabelle.Java_Ext_Dirs "$@"
    39 exec "$JAVA_EXE" -classpath "$(jvmpath "$TARGET")" isabelle.Java_Ext_Dirs \
       
    40   "$(jvmpath "$ISABELLE_HOME/lib/classes/ext")"
    40 
    41