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
{{ message }}
This repository was archived by the owner on Jul 3, 2023. It is now read-only.
Be sure to add a comment to the PR indicating your new changes are ready to review, as GitHub does not generate a
62
62
notification when you git push.
63
63
64
-
### Closing a pull request
64
+
### Merging a pull request
65
65
66
-
Since we run benchmarks as part of CI it's good practice to preserve the commit IDs of the feature branch
66
+
Since we run benchmarks as part of CI it's good practice to preserve the commit IDs of the feature branch
67
67
we've worked on (and benchmarked). Unfortunately, [the github UI does not have support for this](https://github.com/community/community/discussions/4618)
68
68
(it only allows rebase, squash and merge commits to close PRs).
69
-
Therefore, it's recommended to close and merge PRs using the following git CLI invocation:
69
+
Therefore, it's recommended to merge PRs using the following git CLI invocation:
0 commit comments