mathlib3
chore(docs): delete docs/wip.md
#972
Merged
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Overview
Commits
3
Changes
View On
GitHub
chore(docs): delete docs/wip.md
#972
ChrisHughes24
merged 3 commits into
master
from
delete-wip
chore(docs): delete docs/wip.md
6df3cecd
remove link in README
9a89dc0e
kim-em
requested a review
6 years ago
jcommelin
added
ready-to-merge
jcommelin
approved these changes on 2019-05-03
Merge branch 'master' into 'delete-wip'
f2f3dc6e
ChrisHughes24
merged
44386cde
into master
6 years ago
ChrisHughes24
deleted the delete-wip branch
6 years ago
Login to write a write a comment.
Login via GitHub
Reviewers
jcommelin
Assignees
No one assigned
Labels
ready-to-merge
Milestone
No milestone
Login to write a write a comment.
Login via GitHub