From 3b539848c0d8a8dfe3847dc3749a22416bedc39a Mon Sep 17 00:00:00 2001
From: hns <hannesw@gmail.com>
Date: Tue, 12 Jul 2005 09:39:54 +0000
Subject: [PATCH] Add new constructor that takes ignoreCase flag, because it
 can't be set later for app/resource name properties.

---
 src/helma/util/ResourceProperties.java | 18 ++++++++++++++++++
 1 file changed, 18 insertions(+)

diff --git a/src/helma/util/ResourceProperties.java b/src/helma/util/ResourceProperties.java
index d67474f9..8c950674 100644
--- a/src/helma/util/ResourceProperties.java
+++ b/src/helma/util/ResourceProperties.java
@@ -100,6 +100,24 @@ public class ResourceProperties extends Properties {
         forceUpdate();
     }
 
+    /**
+     * Constructs a ResourceProperties retrieving resources from the given
+     * application using the given name to fetch resources and falling back
+     * to the given default properties
+     * @param app application to fetch resources from
+     * @param resourceName name to use when fetching resources from the application
+     * @param defaultProperties default properties
+     * @param ignoreCase ignore case for property keys, setting all keys to lower case
+     */
+    public ResourceProperties(Application app, String resourceName,
+                              ResourceProperties defaultProperties,
+                              boolean ignoreCase) {
+        this(app, resourceName);
+        this.defaultProperties = defaultProperties;
+        this.ignoreCase = ignoreCase;
+        forceUpdate();
+    }
+
     /**
      * Updates the properties regardless of an actual need
      */