From ef29a6d81c3d3c385ac31688c91cf940c2fa0727 Mon Sep 17 00:00:00 2001
From: Gabor Hojtsy <goba@php.net>
Date: Fri, 14 Nov 2003 17:16:02 +0000
Subject: [PATCH] Pointer to the file with JS uncompressed

---
 search.php | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/search.php b/search.php
index 39d46f26f..eb50f8c28 100644
--- a/search.php
+++ b/search.php
@@ -89,6 +89,9 @@ else {
     // Print out common header
     site_header("Search");
     echo "<p>The search feature is accessible via the form elements at the top right of this page.</p>";
+    echo "<p class=\"tip\">We have tried to reduce the size of the function list autocomplete script
+    to the minimum, so you don't need to wait for long to start using this feature. If you are interested
+    in the uncompressed JavaScript source code, look at <a href=\"functions.js.txt\">the functions.js.txt file</a></p>";
     if (FALSE) {
     if (isset($EXPL_LANG)) {
         $lang_input = "  <input type=\"hidden\" name=\"lang\" value=\"{$EXPL_LANG}\" />\n";