lib/scripts/java_ext_dirs
changeset 43521 d477b92109b8
parent 43518 7cad71ca9bcc
child 43522 2562d6c81b03
--- a/lib/scripts/java_ext_dirs	Thu Jun 23 14:52:32 2011 +0200
+++ b/lib/scripts/java_ext_dirs	Thu Jun 23 16:10:22 2011 +0200
@@ -36,5 +36,6 @@
 ## main
 
 JAVA_EXE="${THIS_JAVA:-$ISABELLE_JAVA}"
-exec "$JAVA_EXE" -classpath "$(jvmpath "$TARGET")" isabelle.Java_Ext_Dirs "$@"
+exec "$JAVA_EXE" -classpath "$(jvmpath "$TARGET")" isabelle.Java_Ext_Dirs \
+  "$(jvmpath "$ISABELLE_HOME/lib/classes/ext")"