Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Point to docs.rs for docs. #42

Merged
merged 1 commit into from
Dec 16, 2017

Conversation

waywardmonkeys
Copy link
Contributor

These are more up to date and support versioning.

These are more up to date and support versioning.
Copy link
Member

@emilio emilio left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@emilio
Copy link
Member

emilio commented Dec 16, 2017

@bors-servo r+

@bors-servo
Copy link
Contributor

📌 Commit 02c5511 has been approved by emilio

@bors-servo
Copy link
Contributor

⌛ Testing commit 02c5511 with merge 2302b57...

bors-servo pushed a commit that referenced this pull request Dec 16, 2017
Point to docs.rs for docs.

These are more up to date and support versioning.
@bors-servo
Copy link
Contributor

☀️ Test successful - status-travis
Approved by: emilio
Pushing 2302b57 to master...

@bors-servo bors-servo merged commit 02c5511 into servo:master Dec 16, 2017
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants