From e887fd8959dbbbda083c7f2abb12e4f3ed1a2347 Mon Sep 17 00:00:00 2001
From: Stewart Lord <stewartlord@php.net>
Date: Sat, 1 Jan 2011 20:49:54 +0000
Subject: [PATCH] Search index is now served as an empty array "[]" if
 generated json search index files can't be found.

---
 search-index.php | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

diff --git a/search-index.php b/search-index.php
index ab53c64b9..da0cefeb2 100644
--- a/search-index.php
+++ b/search-index.php
@@ -18,5 +18,11 @@ header("Content-Type: application/javascript");
 ob_start("ob_gzhandler");
 
 echo "$varname = ";
-readfile(dirname(__FILE__) . "/manual/$langcode/$filename.json");
+$file = dirname(__FILE__) . "/manual/$langcode/$filename.json";
+if (is_readable($file)) {
+    readfile($file);
+} else {
+    echo "[]";
+}
+