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

GH-66: Replace 'character string' #67

Open
wants to merge 1 commit into
base: main
Choose a base branch
from
Open

GH-66: Replace 'character string' #67

wants to merge 1 commit into from

Conversation

afs
Copy link
Contributor

@afs afs commented Jan 9, 2025

@afs afs requested review from pfps and doerthe January 10, 2025 08:15
@pfps pfps added the spec:editorial Minor change in the specification (markup, typo, informative text; class 1 or 2) label Jan 10, 2025
Copy link
Contributor

@pfps pfps left a comment

Choose a reason for hiding this comment

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

Looks good as the first change in this area.

@afs
Copy link
Contributor Author

afs commented Jan 17, 2025

@pfps Who merges PRs for this document? A document editor?

@pfps
Copy link
Contributor

pfps commented Jan 17, 2025

As far as I know it has never been clear who should merge PRs. We have had problems with non-editors merging PRs, however.

I thought that the rule for editorial PRs was to let them soak until there was a regular WG meeting and then if there were no problems with them then they were merged (by someone). Is this PR at that stage?

@gkellogg
Copy link
Member

The editors are the ones who are responsible for the document, and generally should be the one merging PRs. There may be exceptions, such as when there is a consensus that a non-editor go ahead with a specific change. For example, I'm not an editor, but I may update the contributors from time to time, and that probably doesn't require an editor to actually push the merge button.

@TallTed
Copy link
Member

TallTed commented Jan 22, 2025

I am strongly of the opinion that only the chosen and committed Editors of each document should be merging PRs, and that only the rarest of changes should be made as a direct commit (without going through a PR) which should likewise only be pushed by an Editor.

Any member of the WG (indeed, any member of the public) may submit such PRs, which the Editor should use their best judgement about merging — usually but not necessarily always waiting for specific approval by the WG, i.e., a spelling correction probably need not wait for group approval, while a normative change probably requires group approval and to have been submitted with/under relevant IPR commitments.

@pfps
Copy link
Contributor

pfps commented Jan 23, 2025

Is there any reason not to merge this PR?

Copy link
Member

@TallTed TallTed left a comment

Choose a reason for hiding this comment

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

lgtm

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
spec:editorial Minor change in the specification (markup, typo, informative text; class 1 or 2)
Projects
None yet
Development

Successfully merging this pull request may close these issues.

4 participants