merged 1.1 branch into head

[mir.git] / source / mir / util / PropertiesManipulator.java

diff --git a/source/mir/util/PropertiesManipulator.java b/source/mir/util/PropertiesManipulator.java
index 25d3e55..a820f57 100755 (executable)
--- a/source/mir/util/PropertiesManipulator.java
+++ b/source/mir/util/PropertiesManipulator.java
@@ -35,11 +35,11 @@ import java.io.LineNumberReader;
 import java.io.OutputStream;
 import java.io.OutputStreamWriter;
 import java.io.PrintWriter;
+import java.util.ArrayList;
 import java.util.HashMap;
 import java.util.Iterator;
 import java.util.List;
 import java.util.Map;
-import java.util.Vector;
 
 import multex.Exc;
 import multex.Failure;
@@ -49,7 +49,7 @@ public class PropertiesManipulator {
   private Map values;
 
   public PropertiesManipulator() {
-    entries = new Vector();
+    entries = new ArrayList();
     values = new HashMap();
   }