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/Migration-Trac-to-Github.md
+7-1Lines changed: 7 additions & 1 deletion
Original file line number
Diff line number
Diff line change
@@ -85,10 +85,16 @@ See also: https://trac.sagemath.org/ticket/30363
85
85
- [Create the PR](https://docs.github.com/en/pull-requests/collaborating-with-pull-requests/proposing-changes-to-your-work-with-pull-requests/creating-a-pull-request)
86
86
- If it is not ready for review, [mark the PR as a "Draft"](https://docs.github.com/en/pull-requests/collaborating-with-pull-requests/proposing-changes-to-your-work-with-pull-requests/changing-the-stage-of-a-pull-request)
87
87
88
-
- For contributing a change that addresses an existing open Issue, **instead of pushing a git branch to a Trac ticket**:
88
+
- For contributing a change that addresses an existing open Issue that has been created on GitHub, **instead of pushing a git branch to a Trac ticket**:
89
89
- same as above
90
90
- [use `Fixes #ISSUENUMBER` to link to an existing issue](https://docs.github.com/en/issues/tracking-your-work-with-issues/linking-a-pull-request-to-an-issue); this will auto-close the linked Issue when the PR is merged.
91
91
92
+
- For contributing a change that addresses an existing open Issue that has been migrated from Trac, **instead of pushing a git branch to a Trac ticket**:
93
+
- Pull the branch from your read-only `trac` remote (see section *One time action: Instead of adding a git remote named trac*) as you use to do before.
94
+
- Edit and commit your changes
95
+
- Push the branch to the remote named `origin`, i.e., to your fork
96
+
- Follow the instructions above from there
97
+
92
98
- For finding PRs that are waiting for review, **instead of using Trac ticket reports**:
93
99
- [filter PRs by review status](https://docs.github.com/en/issues/tracking-your-work-with-issues/filtering-and-searching-issues-and-pull-requests#filtering-pull-requests-by-review-status)
0 commit comments