# HG changeset patch
# User wenzelm
# Date 1295632900 -3600
# Node ID ad5474a8374b779b38ce23b3350a7741d2c99d6e
# Parent  55b16bd82142195759e2703ab0421836d191315a
java/scala: default to UTF-8;

diff -r 55b16bd82142 -r ad5474a8374b lib/Tools/java
--- 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
 
diff -r 55b16bd82142 -r ad5474a8374b lib/Tools/scala
--- a/lib/Tools/scala	Fri Jan 21 17:33:55 2011 +0100
+++ b/lib/Tools/scala	Fri Jan 21 19:01:40 2011 +0100
@@ -9,4 +9,4 @@
 [ -e "$ISABELLE_HOME/Admin/build" ] && { "$ISABELLE_HOME/Admin/build" jars || exit $?; }
 
 CLASSPATH="$(jvmpath "$CLASSPATH")"
-exec "$SCALA_HOME/bin/scala" "$@"
+exec "$SCALA_HOME/bin/scala" -Dfile.encoding=UTF-8 "$@"