-
Notifications
You must be signed in to change notification settings - Fork 386
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
Update contribution guides #2624
Update contribution guides #2624
Conversation
Too many arbitrary changes that would need discussion. Perhaps you could try again with the absolute minimal changes required to merge the files? Otherwise we will get to it: even the report about the duplication is very helpful. |
@semorrison I'd love to make minimal changes, but the sentences are interrelated - can't change one without changing the other. I've fixed some points that you've mentioned and replied to others. Sorry if I did something wrong - please let me know if it needs more improvements. |
The basic problem is that doc/contributions.md is the new version that should take priority, and was recently written by Leo. By merging it into the other document is has essentially been lost. I think the only viable path to combining these documents is:
But really anything that is much beyond deleting |
|
Updated https://github.com/DenisGorbachev/lean4/blob/contribution-guidelines/CONTRIBUTING.md:
Reason for replacement: since CONTRIBUTING.md should help people who want to contribute, it's better to start with a welcome message. Is it correct? If yes - should I open a new PR or would you like to reopen the current one? |
Please revert the change from the "replaced:" bullet point. That's a significant editorial change! |
Done |
awaiting-review (commenting to change the label) |
@semorrison Is there anything else that should be done on this PR? |
In principle I'm happy now, but the problem is that there is a slide deck for the community meeting that uses the old URL, so I'm very hesitant to merge now. :-) |
Sorry, on further reflection the right solution is to leave |
Understood :) Actually, https://lean-lang.org/lean4/doc/contributions.html returns 404. This is because Meanwhile, Let me know if you'd still like to move the text back to |
Also, is it OK to provide additional info (like I've done in the previous comment), or would it be better to just implement your suggestions immediately? |
Thanks for your patience on this one, @DenisGorbachev! Just checking what we want to do here. |
@semorrison Is there any way I can help regarding this PR? |
@semorrison Would you like me to do anything else on this PR? |
External Contribution Guidelines.
Summary
Currently, there are two guides: CONTRIBUTING.md and doc/contributions.md.
It would be better to merge the guides into a single CONTRIBUTING.md, and link to that file from PULL_REQUEST_TEMPLATE.md.
Notes
I tried to preserve the original wording, but I've shortened some paragraphs & removed ambiguous sentences. Please correct if wrong.
For review, it may be easier to read the final files instead of the diffs.
Questions