This is the mail archive of the
java-patches@gcc.gnu.org
mailing list for the Java project.
Patch: FYI: Properties file encoding
- To: Java Patch List <java-patches at gcc dot gnu dot org>
- Subject: Patch: FYI: Properties file encoding
- From: Tom Tromey <tromey at redhat dot com>
- Date: 06 Sep 2001 11:27:10 -0600
- Reply-To: tromey at redhat dot com
The spec requires that a property file use the ISO-8859-1 encoding.
However, we weren't doing this. We were using the default encoding.
Tom
Index: ChangeLog
from Tom Tromey <tromey@redhat.com>
* java/util/Properties.java: Re-merged from Classpath.
Index: java/util/Properties.java
===================================================================
RCS file: /cvs/gcc/gcc/libjava/java/util/Properties.java,v
retrieving revision 1.8
diff -u -r1.8 Properties.java
--- java/util/Properties.java 2001/03/19 23:00:17 1.8
+++ java/util/Properties.java 2001/09/05 20:18:15
@@ -1,5 +1,5 @@
/* java.util.Properties
- Copyright (C) 1998, 1999, 2000 Free Software Foundation, Inc.
+ Copyright (C) 1998, 1999, 2000, 2001 Free Software Foundation, Inc.
This file is part of GNU Classpath.
@@ -61,7 +61,8 @@
* of <code>get/put</code>.
*
* @see PropertyResourceBundle
- * @author Jochen Hoenicke */
+ * @author Jochen Hoenicke
+ */
public class Properties extends Hashtable
{
/**
@@ -128,8 +129,9 @@
* from the input. */
public void load(InputStream inStream) throws IOException
{
+ // The spec says that the file must be encoded using ISO-8859-1.
BufferedReader reader =
- new BufferedReader(new InputStreamReader(inStream));
+ new BufferedReader(new InputStreamReader(inStream, "ISO-8859-1"));
String line;
while ((line = reader.readLine()) != null)
@@ -302,7 +304,9 @@
*/
public void store(OutputStream out, String header) throws IOException
{
- PrintWriter writer = new PrintWriter(out);
+ // The spec says that the file must be encoded using ISO-8859-1.
+ PrintWriter writer
+ = new PrintWriter(new OutputStreamWriter (out, "ISO-8859-1"));
if (header != null)
writer.println("#" + header);
writer.println("#" + new Date().toString());