file.encoding=UTF-8 for java.ext.dirs, to agree with java runtime invocation;
authorwenzelm
Thu May 10 22:49:12 2012 +0200 (2012-05-10)
changeset 4787845bfbd7d6e58
parent 47876 0521ee2e504d
child 47879 de5602637ab4
file.encoding=UTF-8 for java.ext.dirs, to agree with java runtime invocation;
src/Tools/JVM/java_ext_dirs
     1.1 --- a/src/Tools/JVM/java_ext_dirs	Thu May 10 20:49:30 2012 +0200
     1.2 +++ b/src/Tools/JVM/java_ext_dirs	Thu May 10 22:49:12 2012 +0200
     1.3 @@ -17,7 +17,7 @@
     1.4  
     1.5  ## main
     1.6  
     1.7 -isabelle_jdk java \
     1.8 +isabelle_jdk java -Dfile.encoding=UTF-8 \
     1.9    -classpath "$(jvmpath "$ISABELLE_HOME/src/Tools/JVM/java_ext_dirs.jar")" \
    1.10    isabelle.Java_Ext_Dirs "$(jvmpath "$ISABELLE_HOME/lib/classes/ext")" 2>/dev/null
    1.11