Skip to content

Auto merge of #11865 - yuxqiu:map_unwrap_or_default, r=Jarcho #15467

Auto merge of #11865 - yuxqiu:map_unwrap_or_default, r=Jarcho

Auto merge of #11865 - yuxqiu:map_unwrap_or_default, r=Jarcho #15467

Triggered via push December 30, 2023 16:37
Status Success
Total duration 1m 7s
Artifacts

clippy_dev.yml

on: push
clippy_dev
51s
clippy_dev
bors dev test finished
0s
bors dev test finished
bors dev test finished
0s
bors dev test finished
Fit to window
Zoom out
Zoom in