You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Copy file name to clipboardExpand all lines: docs/source/contributing/contributing.md
+3-1Lines changed: 3 additions & 1 deletion
Display the source diff
Display the rich diff
Original file line number
Diff line number
Diff line change
@@ -60,14 +60,16 @@ This outlines the process for getting changes to the repo2docker project merged.
60
60
Getting consensus with the community is a great way to save time later.
61
61
3. Make edits in [your fork](https://help.github.com/en/articles/fork-a-repo) of the [repo2docker repository](https://github.com/jupyterhub/repo2docker).
62
62
4. Make a [pull request](https://help.github.com/en/articles/about-pull-requests).
63
-
Read the [next section](#guidelines-to-getting-a-pull-request-merged) for guidelines for both reviewers and contributors on merging a PR.
63
+
Read the [next section](guidelines-to-getting-a-pull-request-merged) for guidelines for both reviewers and contributors on merging a PR.
64
64
6. Wait for a community member to merge your changes.
65
65
Remember that **someone else must merge your pull request**.
66
66
That goes for new contributors and long term maintainers alike.
67
67
Because `main` is continuously deployed to mybinder.org it is essential
68
68
that `main` is always in a deployable state.
69
69
7. (optional) Deploy a new version of repo2docker to mybinder.org by [following these steps](http://mybinder-sre.readthedocs.io/en/latest/deployment/how.html)
70
70
71
+
(guidelines-to-getting-a-pull-request-merged)=
72
+
71
73
## Guidelines to getting a Pull Request merged
72
74
73
75
These are not hard rules to be enforced by 🚓 but they are suggestions written by the repo2docker maintainers to help complete your contribution as smoothly as possible for both you and for them.
0 commit comments