From 8572085cc721a17801b8e7bfdd61d661ef4cc98c Mon Sep 17 00:00:00 2001
From: Araq <rumpf_a@web.de>
Date: Mon, 5 Mar 2018 13:16:46 +0100
Subject: [PATCH] fixes #7294; Nim doc search feature

---
 config/nimdoc.cfg | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/config/nimdoc.cfg b/config/nimdoc.cfg
index 2800bc581a..231aa54742 100644
--- a/config/nimdoc.cfg
+++ b/config/nimdoc.cfg
@@ -75,7 +75,7 @@ doc.body_toc = """
 <div class="row">
   <div class="three columns">
   <div>
-    Search: <input type="text" id="searchInput"
+    Search: <input type="text" id="searchInputDiv"
       onkeyup="search()" />
   </div>
   $tableofcontents
@@ -109,7 +109,7 @@ doc.body_toc_group = """
       </li>
     </ul>
   </div>
-  <div id="searchInput">
+  <div id="searchInputDiv">
     Search: <input type="text" id="searchInput"
       onkeyup="search()" />
   </div>
@@ -139,7 +139,7 @@ doc.body_toc_group = """
     <ul class="simple">
     </ul>
   </div>
-  <div id="searchInput">
+  <div id="searchInputDiv">
     Search: <input type="text" id="searchInput"
       onkeyup="search()" />
   </div>
@@ -364,10 +364,10 @@ dd > pre {
   table-layout: fixed; }
 
 /* Nim search input */
-div#searchInput {
+div#searchInputDiv {
   margin-bottom: 8px;
 }
-div#searchInput input#searchInput {
+div#searchInputDiv input#searchInput {
   width: 10em;
 }
 div.search-groupby {