Skip to content

Remove an unnecessary Option#97616

Merged
bors merged 1 commit intorust-lang:masterfrom
TaKO8Ki:remove-unnecessary-option
Jun 1, 2022
Merged

Remove an unnecessary `Option`#97616
bors merged 1 commit intorust-lang:masterfrom
TaKO8Ki:remove-unnecessary-option

Commits

Commits on Jun 1, 2022