1 files changed, 11 insertions, 0 deletions

diff --git a/manual/gsearch.js b/manual/gsearch.js
new file mode 100644
index 0000000000..9b5e3f7aa1
--- /dev/null
+++ b/manual/gsearch.js
@@ -0,0 +1,11 @@
+function gsearch() {
+    var expr=/(.*)\/([^/]+)$/;
+    var loc = expr.exec(window.location)[1];
+    document.getElementById("gsearch").innerHTML = ''
+    + '<form action="http://www.google.com/search">'
+    + 'Search this manual '
+    + '<input name="as_q" size="30">'
+    + '<input value="Google it" type="submit">'
+    + '<input type="hidden" name="as_sitesearch" value="' + loc + '">'
+    + '</form>';
+}