Improve search result tab handling#80382

Merged

bors merged 1 commit intorust-lang:masterfrom

GuillaumeGomez:search-result-tab-picking

Jan 19, 2021

Commits on Dec 30, 2020

If the current search result tab is empty, it picks the first non-empty one. If all are empty, the current one doesn't change.
GuillaumeGomez
committed