diff options
| author | Vincent Rouvreau <10407034+VincentRouvreau@users.noreply.github.com> | 2020-03-02 13:50:35 +0100 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-03-02 13:50:35 +0100 |
| commit | d2943b9e7311c8a3d8a4fb379c39b15497481b9c (patch) | |
| tree | 2745f64abd58cd05620c3ae8092bc33670b54c51 /.github/how_to_use_github_to_contribute_to_gudhi.md | |
| parent | f8c251b1c1b7a1c8c36e77f56cda1fd41245adb7 (diff) | |
[skip ci] add a note on next_release.md file
Diffstat (limited to '.github/how_to_use_github_to_contribute_to_gudhi.md')
| -rw-r--r-- | .github/how_to_use_github_to_contribute_to_gudhi.md | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/.github/how_to_use_github_to_contribute_to_gudhi.md b/.github/how_to_use_github_to_contribute_to_gudhi.md index 0a6133b7..6ab05e36 100644 --- a/.github/how_to_use_github_to_contribute_to_gudhi.md +++ b/.github/how_to_use_github_to_contribute_to_gudhi.md @@ -90,6 +90,8 @@ Because of `-u`, it will remember where you like to push this branch, and next t Possibly iterate a few times, add more commits and push them. ## Your pull request is ready +Do not forget to update `.github/next_release.md` to announce your development in the next release note. + Get your web browser to https://github.com/LOGIN/gudhi-devel, click on the button that says **Branch: some-name** (below the number of commits, above the list of files) and select the branch you are so proud of. Click on **New pull request** next to it. |