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.

Sign up for GitHub

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

Jump to bottom

Require language extensions in a more user-friendly manner #1030

Merged
merged 3 commits into from
Feb 8, 2020
Merged

Require language extensions in a more user-friendly manner #1030

merged 3 commits into from
Feb 8, 2020

Conversation

parsonsmatt
Copy link
Collaborator

@parsonsmatt parsonsmatt commented Feb 7, 2020 •
edited
Loading

Before submitting your PR, check that you've:

After submitting your PR:

  • Update the Changelog.md file with a link to your PR
  • Check that CI passes (or if it fails, for reasons unrelated to your change, like CI timeouts)

@erikd
Copy link
Contributor

erikd commented Feb 7, 2020

I keep and eye on Persistent because I use it. I read PR titles to get and idea of what is going on.

Sorry this is not a useful PR title :).

@parsonsmatt
Copy link
Collaborator Author

oh crap, sorry, i meant to edit this before making the PR :|

@parsonsmatt parsonsmatt changed the title stuff Require language extensions in a more user-friendly manner Feb 7, 2020
@parsonsmatt parsonsmatt merged commit b7ec5ab into master Feb 8, 2020
@parsonsmatt parsonsmatt mentioned this pull request Feb 8, 2020
Closed
@parsonsmatt parsonsmatt deleted the require-extensions branch March 31, 2020 15:23
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
2 participants
@parsonsmatt @erikd