feat: tag linter warnings for recordLints#13844

wkrozowski wants to merge 1 commit into

leanprover:masterleanprover/lean4:masterfrom

wkrozowski:feat/linter-message-tagwkrozowski/lean4:feat/linter-message-tagCopy head branch name to clipboard