Skip to content

Fix missing renaming for #titles into #search-tabs#106153

Merged
bors merged 2 commits intorust-lang:masterfrom
GuillaumeGomez:search-tabs-headers
Dec 26, 2022
Merged

Fix missing renaming for #titles into #search-tabs#106153
bors merged 2 commits intorust-lang:masterfrom
GuillaumeGomez:search-tabs-headers

Commits

Commits on Dec 26, 2022