diff --git a/doc/gmsh.html b/doc/gmsh.html
index da00d5284a70f0de4436870e8b5606c38dd9c466..74f18dff9075f966df944fcf0b886993e7d3da61 100644
--- a/doc/gmsh.html
+++ b/doc/gmsh.html
@@ -213,17 +213,6 @@ on <a href="https://gitlab.onelab.info/gmsh/gmsh/issues"
 ><code>https://gitlab.onelab.info/gmsh/gmsh/issues</code></a>.
 </p>
 
-<form method="get" action="http://onelab.info/search/search.cgi">
-<input size="30" name="q" value="">&nbsp;
-<input type="submit" value="Search!">&nbsp;
-<input type="hidden" name="ps" value="10">
-<select name="ul">
-  <option value="/" SELECTED>Whole site
-  <option value="/doc/">Documentation
-  <option value="/pipermail/gmsh">Mailing list archives
-</select>
-</form>
-
 <h2><a name="Licensing"></a>Licensing</h2>
 
 <p>