Skip to content
This repository has been archived by the owner on Jul 24, 2024. It is now read-only.

[Merged by Bors] - chore(logic/relation): rename to permit dot notation #10105

Closed
wants to merge 2 commits into from
Closed

[Merged by Bors] - chore(logic/relation): rename to permit dot notation #10105

wants to merge 2 commits into from

Conversation

eric-wieser
Copy link
Member

Open in Gitpod

@eric-wieser eric-wieser force-pushed the eric-wieser/equivalence-dot-notation branch from 679e884 to 94f6f17 Compare November 2, 2021 11:24
@eric-wieser eric-wieser added the awaiting-review The author would like community review of the PR label Nov 2, 2021
kmill
kmill approved these changes Nov 2, 2021
View reviewed changes
Copy link
Collaborator

@kmill kmill left a comment

Choose a reason for hiding this comment

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

Thanks for looking into this

bryangingechen
bryangingechen approved these changes Nov 3, 2021
View reviewed changes
Copy link
Collaborator

@bryangingechen bryangingechen left a comment

Choose a reason for hiding this comment

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

Thanks!
bors r+

@github-actions github-actions bot added ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) and removed awaiting-review The author would like community review of the PR labels Nov 3, 2021
bors bot pushed a commit that referenced this pull request Nov 3, 2021
@eric-wieser
chore(logic/relation): rename to permit dot notation (#10105)
00a1022
@bryangingechen bryangingechen changed the title chore(logic/relation): rename to permit dot notation [Merged by Bors] - chore(logic/relation): rename to permit dot notation Nov 3, 2021
@bryangingechen
Copy link
Collaborator

bors crashed, but this was successfully merged.

@bors bors bot deleted the eric-wieser/equivalence-dot-notation branch November 3, 2021 20:02
ericrbg pushed a commit that referenced this pull request Nov 9, 2021
@eric-wieser @ericrbg
chore(logic/relation): rename to permit dot notation (#10105)
b3ee0ab
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Reviewers

@kmill kmill kmill approved these changes

@bryangingechen bryangingechen bryangingechen approved these changes

Assignees
No one assigned
Labels
ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.)
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
3 participants
@eric-wieser @bryangingechen @kmill