if $c:expr { Some($r:expr) } else { None } =>> $c.then(|| $r)#108079
Merged
bors merged 1 commit intorust-lang:masterfrom Feb 15, 2023
Merged
`if $c:expr { Some($r:expr) } else { None }` =>> `$c.then(|| $r)`#108079bors merged 1 commit intorust-lang:masterfrom
bors merged 1 commit intorust-lang:masterfrom
