Join GitHub today
Always display google search option #1391
If you type a search term and no results show up, you're given an option to do a google search for that term. However, that option isn't available when some results turned up.
I think the option to do a google search should always be present because the found results might not be what the user is looking for (e.g. I searched for "binder"), yet the site might still have the word used somewhere the search index didn't grab it, so a google search would still be useful.
referenced this issue
Jul 5, 2017
I have been testing with this. It looks easy in principle, just a matter of commenting out the part of the JS in search.js that adds this only if there are no results. However, there are some minor and some major problems. Minor one is the message, which is "Not found". That can be changed. Major one is that the message is not "added", but rather pops up in a separate div when the drop-down menu is closed. That's not noticed with no result because there's no result.