mathlib3
chore(tactic/lint): typo
#2253
Merged
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Overview
Commits
2
Changes
View On
GitHub
chore(tactic/lint): typo
#2253
mergify
merged 2 commits into
master
from
time-class-typo
chore(tactic/lint): typo
5148f2db
gebner
approved these changes on 2020-03-27
gebner
added
ready-to-merge
Merge branch 'master' into time-class-typo
8d7dfd22
mergify
merged
451de279
into master
6 years ago
bryangingechen
deleted the time-class-typo branch
6 years ago
Login to write a write a comment.
Login via GitHub
Reviewers
gebner
Assignees
No one assigned
Labels
ready-to-merge
Milestone
No milestone
Login to write a write a comment.
Login via GitHub