make it easier to filter properties (case insensitive)

11 years ago · f597fdb602
parent c833d02cf5
commit f597fdb602
1 changed files with 1 additions and 1 deletions
--- a/htroot/ConfigProperties_p.html
+++ b/htroot/ConfigProperties_p.html
@ -18,7 +18,7 @@
 			  key=document.getElementById("key").value;
 			  while(node!=null){
 					  if(node.nodeType==1 && node.nodeName.toLowerCase()=="option"){
-							  if(key!="" && node.firstChild.nodeValue.indexOf(key)==-1){
+							  if(key!="" && node.firstChild.nodeValue.toLowerCase().indexOf(key.toLowerCase())==-1){
 									  node.setAttribute("class", "filtered");
 							  }else{
 									  node.setAttribute("class", "");