-
Notifications
You must be signed in to change notification settings - Fork 37
Set EIP number immediately before merging new EIP pull requests #64
Comments
I will work on it. |
I suggest that authors just send a comment of the form:
where XXXX is the EIP number. This will perform the rename and other formatting on the spot. If no number is present when it would be merged, then the PR number can be used, meaning that the comment can be used for cases of number gaming. |
What's the advantage of assigning the number before merging? @MicahZoltu has mentioned he'd like to avoid assigning EIP numbers until the EIP is merged, and I'd tend to agree with that. I was sorta envisioning a bors-style bot that creates the merge commit and pushes it to the default branch. |
This one confused me. am I wrong if I said that only editors assign EIP number (manually ?) ? |
Currently editors manually assign EIP numbers. This issue proposes we change that, but I am a bit worried about people gaming the system if it becomes fully automated. |
See my suggestion at #64 (comment) This would prevent number gaming by allowing EIP editors to manually change the EIP number. |
I suggest to talk about it during the next call and agree in one action (if any) |
Ideally I'd like to avoid assigning an EIP number until the PR is merged, so my preference would be for a comment allowing EIP editors to override the number without changing the file itself. Something like:
That said, I think an easier to implement solution would be to only auto-assign a number on merge if a number isn't already set. |
Originally from #55
Immediately before merging (IMO, ideally in the merge commit itself) set the EIP number in the preamble and rename the markdown file. How that number is determined probably needs to be discussed here.
The text was updated successfully, but these errors were encountered: