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

RFC: rename_maybe_pointer #152

Merged
merged 2 commits into from
Aug 6, 2019
Merged

RFC: rename_maybe_pointer #152

merged 2 commits into from
Aug 6, 2019

Conversation

Theodus
Copy link
Contributor

@Theodus Theodus commented Jul 30, 2019 •
edited
Loading

Rendered

Closes #48

@SeanTAllen
Copy link
Member

We agreed at Sync that NullablePointer is the name we would like to use.

@Theodus Theodus added the status - final comment period The RFC is finalized. Waiting for final comments. label Jul 30, 2019
@Theodus Theodus mentioned this pull request Jul 30, 2019
Closed
@SeanTAllen SeanTAllen added status - ready for vote The RFC is ready to be voted on. and removed status - final comment period The RFC is finalized. Waiting for final comments. labels Aug 6, 2019
@SeanTAllen SeanTAllen merged commit 31efdc0 into master Aug 6, 2019
@SeanTAllen SeanTAllen deleted the maybe-pointer branch August 6, 2019 16:30
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
status - ready for vote The RFC is ready to be voted on.
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

Change name of MaybePointer in builtin.
2 participants
@Theodus @SeanTAllen