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