Fixed the search javascript, which was a bit broken.

Rev: tutorial/html.pike:1.40

tutorial/html.pike

@@ -345,6 +345,7 @@ function do_search()
   matches=0;
 
   for(a in f) {
+    a+='';
     i=a.indexOf(text);
     if(i != -1 && (i==0 || a.charAt(i-1)=='.') && (i+text.length == a.length || a.charAt(i+text.length) == '.')) {
        found=f[a];