manual/gsearch.js

   1 function gsearch() {
   2     var expr=/(.*)\/([^/]+)$/;
   3     var loc = expr.exec(window.location)[1];
   4     document.getElementById("gsearch").innerHTML = ''
   5     + '<form action="http://www.google.com/search">'
   6     + 'Search this manual '
   7     + '<input name="as_q" size="30">'
   8     + '<input value="Google it" type="submit">'
   9     + '<input type="hidden" name="as_sitesearch" value="' + loc + '">'
  10     + '</form>';
  11 }