Skip to content

Remove unneeded extra chars to reduce search-index size#56709

Merged
bors merged 2 commits intorust-lang:masterfrom
GuillaumeGomez:reduce-search-index
Dec 14, 2018
Merged

Remove unneeded extra chars to reduce search-index size#56709
bors merged 2 commits intorust-lang:masterfrom
GuillaumeGomez:reduce-search-index

Commits

Commits on Dec 11, 2018

Commits on Dec 13, 2018