bot fix style (comment)

[Merged by Bors] - chore: remove some `Setoid.r` #5777

Sign in to view logs

Triggered via issue October 9, 2024 16:48

commented on #16258 7817d20

Status Skipped

Total duration 2s

Artifacts –

bot_fix_style_comment.yaml

on: issue_comment

Fix style issues from lint