From addc8ca839a0ff879a5a972fa1a56762d20bcd42 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Johan=20Sundstr=C3=B6m?= <oyasumi@gmail.com>
Date: Thu, 27 Jan 2000 02:47:04 +0100
Subject: [PATCH] Fixed the search javascript, which was a bit broken.

Rev: tutorial/html.pike:1.40
---
 tutorial/html.pike | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/tutorial/html.pike b/tutorial/html.pike
index 646708a5eb..c45cde3148 100644
--- a/tutorial/html.pike
+++ b/tutorial/html.pike
@@ -343,8 +343,9 @@ function do_search()
 
   top.display.document.write('<h2>Searching for '+text+'</h2>\\n');
   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];
-- 
GitLab