function gsearch() { var expr=/(.*)\/([^/]+)$/; var loc = expr.exec(window.location)[1]; document.getElementById("gsearch").innerHTML = '' + '
' + 'Search this manual ' + '' + '' + '' + '
'; }