diff --git a/htroot/ConfigProperties_p.html b/htroot/ConfigProperties_p.html index 39e4a767f..da5e3c958 100644 --- 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", "");