Right now, our search disables the search box that comes with mediawiki on the search results page. That means that searching again for a similar term requires annoying copy and pages into the top box. We should add some javascript to put the search term into that box. It doesn't look like it's possible to do it through php, though that could be researched more deeply.
Right now, our search disables the search box that comes with mediawiki on the search results page. That means that searching again for a similar term requires annoying copy and pages into the top box. We should add some javascript to put the search term into that box. It doesn't look like it's possible to do it through php, though that could be researched more deeply.