move-decls (comment)

[Merged by Bors] - feat: rewrite the copyright header check in Lean #5983

Sign in to view logs

Triggered via issue June 23, 2024 07:52

kim-em

commented on #13240 756e653

Status Skipped

Total duration 2s

Artifacts –

move_decl_comment.yml

on: issue_comment

move-decls-add-comment