in website/static/cdocs/search/search.js [1:22]
function convertToId(search)
{
var result = '';
for (i=0;i<search.length;i++)
{
var c = search.charAt(i);
var cn = c.charCodeAt(0);
if (c.match(/[a-z0-9\u0080-\uFFFF]/))
{
result+=c;
}
else if (cn<16)
{
result+="_0"+cn.toString(16);
}
else
{
result+="_"+cn.toString(16);
}
}
return result;
}