move-decls (comment)

[Merged by Bors] - feat(lint-style): fix `update-style-exceptions.py`; produce human-readable output by default #5988

Sign in to view logs

Triggered via issue June 23, 2024 08:01

mathlib-bors[bot]

commented on #14012 ca9e9db

Status Skipped

Total duration 2s

Artifacts –

move_decl_comment.yml

on: issue_comment

move-decls-add-comment