mathlib3
feat(tactic/lint): silent linting
#1580
Merged
Overview
Commits
6
Changes
View On GitHub
Commits
  • feat(tactic/lint): silent linting
    robertylewis committed 6 years ago
  • doc(tactic/lint): doc silent linting and nolint features
    robertylewis committed 6 years ago
  • fix test
    robertylewis committed 6 years ago
  • change notation for silent linting
    robertylewis committed 6 years ago
  • style(tactic/lint): remove commented lines
    robertylewis committed 6 years ago
  • Merge branch 'master' into lint
    mergify[bot] committed 6 years ago
FAQ Terms Privacy Refunds Impressum
Loading