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

[func.wrap.func] Remove declarations already in [functional.syn] #4035

Closed
wants to merge 1 commit into from
Closed

[func.wrap.func] Remove declarations already in [functional.syn] #4035

wants to merge 1 commit into from

Conversation

JohelEGP
Copy link
Contributor

@JohelEGP JohelEGP commented Jun 11, 2020 •
edited

Partially addresses #4041.

@jensmaurer jensmaurer added decision-required A decision of the editorial group (or the Project Editor) is required. needs rebase The pull request needs a git rebase to resolve merge conflicts. labels Sep 19, 2020
@jensmaurer
Copy link
Member

See #4037

@jensmaurer jensmaurer removed needs rebase The pull request needs a git rebase to resolve merge conflicts. decision-required A decision of the editorial group (or the Project Editor) is required. labels Dec 4, 2020
@jensmaurer
Copy link
Member

Editorial meeting: Remove redundancy = apply, but add a cross-reference in functional.syn for swap and operator==.

@jensmaurer jensmaurer added the changes requested Changes to the wording or approach have been requested and not yet applied. label Dec 4, 2020
@JohelEGP JohelEGP mentioned this pull request Dec 4, 2020
Closed
@JohelEGP JohelEGP closed this Dec 5, 2020
@JohelEGP
Copy link
Contributor Author

JohelEGP commented Dec 5, 2020 •
edited

Could someone reopen this for me, or should I make a new PR? I messed up the initial fixup for the requested changes, but it's fine now: master...johelegp:func.wrap.func.
If the button to reopen doesn't work, this may help: How to reopen a pull-request after a force-push?

@jensmaurer
Copy link
Member

jensmaurer commented Dec 6, 2020 •
edited

In order to follow the procedure, you need to force-push first, then I can re-open. Alternatively, create a new pull request.

@JohelEGP
Copy link
Contributor Author

JohelEGP commented Dec 6, 2020

I'll do the latter. The branch is already rebased on master, but that's not reflected here.

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
changes requested Changes to the wording or approach have been requested and not yet applied.
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
2 participants
@JohelEGP @jensmaurer