Mathlib v3 is deprecated. Go to Mathlib v4

Def escape_workflow_command

Modification history

2022-01-11 13:55
src/tactic/lint/frontend.lean
feat(scripts/lint_mathlib): implement github annotations for mathlib linters (#11345) …
Added escape_workflow_commandView on Github →