| changeset 41622 | ad5474a8374b |
| parent 41380 | 92237dee0f29 |
| child 43521 | d477b92109b8 |
--- a/lib/Tools/java Fri Jan 21 17:33:55 2011 +0100 +++ b/lib/Tools/java Fri Jan 21 19:01:40 2011 +0100 @@ -9,8 +9,8 @@ JAVA_EXE="${THIS_JAVA:-$ISABELLE_JAVA}" if "$JAVA_EXE" -server >/dev/null 2>/dev/null then - exec "$JAVA_EXE" -server "$@" + exec "$JAVA_EXE" -Dfile.encoding=UTF-8 -server "$@" else - exec "$JAVA_EXE" "$@" + exec "$JAVA_EXE" -Dfile.encoding=UTF-8 "$@" fi