Update PR instructions in CONTRIBUTING.md#31
Update PR instructions in CONTRIBUTING.md#31jcailler wants to merge 1 commit intoGoelandProver:masterfrom
Conversation
|
FYI as the go source code has not been modified, we don't need to run the full CI on this PR. (see e.g., on the maintainer section of the contributing file) |
|
To be honest, I'm not sure it's our job to give these tips. I'm not against contributors having their cheatsheet, or even linking to a github command cheatsheet inside the contribution file, e.g., this one for instance. My initial thoughts: I don't think we should keep the "create a branch" section, but maybe we can keep the creation of a PR / rebasing comments by factoring them through a specific section for pull requests. But the text would need to be reworked before. For instance, you should push your branch, then open a PR. |
|
I'm converting this PR to draft until further discussions / progress. |
|
Your branch seems to be in a strange state with the merge commit and everything. |
Update Contributing.md and .gitignore Remarks
| ``` | ||
|
|
||
| where `remote` is the name of the remote fetching `git@github.com:GoelandProver/Goeland.git` (which can be found using `git remote -v`) | ||
|
|
There was a problem hiding this comment.
I feel like a transition is missing between these two paragraphs. Maybe something like: "If you want to open a pull request, you should roughly follow these steps:"
Add git instruction for contributors