java/scala: default to UTF-8;
authorwenzelm
Fri Jan 21 19:01:40 2011 +0100 (2011-01-21)
changeset 41622ad5474a8374b
parent 41621 55b16bd82142
child 41623 f5619d83d0e3
java/scala: default to UTF-8;
lib/Tools/java
lib/Tools/scala
     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  
     2.1 --- a/lib/Tools/scala	Fri Jan 21 17:33:55 2011 +0100
     2.2 +++ b/lib/Tools/scala	Fri Jan 21 19:01:40 2011 +0100
     2.3 @@ -9,4 +9,4 @@
     2.4  [ -e "$ISABELLE_HOME/Admin/build" ] && { "$ISABELLE_HOME/Admin/build" jars || exit $?; }
     2.5  
     2.6  CLASSPATH="$(jvmpath "$CLASSPATH")"
     2.7 -exec "$SCALA_HOME/bin/scala" "$@"
     2.8 +exec "$SCALA_HOME/bin/scala" -Dfile.encoding=UTF-8 "$@"