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

Editorial: replace a few stray GetReferencedName invocations / re-define "super-reference" #2220

Merged
merged 2 commits into from
Nov 3, 2020

Conversation

bakkot
Copy link
Contributor

@bakkot bakkot commented Nov 2, 2020

GetReferencedName was removed by #2085, but while that PR was open #2030 landed and introduced three new references to it, which we missed. This PR fixes those three references.

Also, #2085 removed the id for "super-reference"; this restores that as an oldid on the definition of "Super Reference Record".

Thanks to @jmdyck for pointing these out.

@bakkot bakkot changed the title Editorial: replace a few stray GetReferencedName invocations Editorial: replace a few stray GetReferencedName invocations / re-define "super-reference" Nov 2, 2020
@ljharb ljharb requested review from michaelficarra and syg November 2, 2020 22:47
@ljharb ljharb self-assigned this Nov 2, 2020
@ljharb ljharb merged commit 5657da4 into master Nov 3, 2020
@ljharb ljharb deleted the get-ref-name branch November 3, 2020 22:56
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging this pull request may close these issues.

4 participants