Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

change(docs): Document how to get external PRs to merge #6252

Merged
merged 2 commits into from
Mar 1, 2023
Merged

change(docs): Document how to get external PRs to merge #6252

merged 2 commits into from
Mar 1, 2023

Conversation

teor2345
Copy link
Contributor

@teor2345 teor2345 commented Feb 28, 2023 •
edited
Loading

Motivation

We need instructions for getting PRs from external repositories to merge, because #4529 is still something we need to fix in CI.

Review

This is a routine developer documentation update.

Reviewer Checklist

  • Will the PR name make sense to users?
    • Does it need extra CHANGELOG info? (new features, breaking changes, large changes)
  • Are the PR labels correct?
  • Do the instructions make sense?

@teor2345 teor2345 added A-docs Area: Documentation A-devops Area: Pipelines, CI/CD and Dockerfiles C-enhancement Category: This is an improvement P-Medium ⚡ C-trivial Category: A trivial change that is not worth mentioning in the CHANGELOG labels Feb 28, 2023
@teor2345 teor2345 requested a review from a team as a code owner February 28, 2023 20:00
@teor2345 teor2345 self-assigned this Feb 28, 2023
@teor2345 teor2345 requested review from upbqdn and removed request for a team February 28, 2023 20:00
upbqdn
upbqdn previously approved these changes Feb 28, 2023
View reviewed changes
Copy link
Member

@upbqdn upbqdn left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks for writing this down for the team.

book/src/dev/continuous-integration.md Outdated Show resolved Hide resolved
@teor2345 @upbqdn
Fix typos
30cd0d7 
Co-authored-by: Marek <mail@marek.onl>
mergify bot added a commit that referenced this pull request Mar 1, 2023
@mergify
Merge of #6252
c37190a
@mergify mergify bot mentioned this pull request Mar 1, 2023
Closed
@mergify mergify bot merged commit dde63d2 into main Mar 1, 2023
@mergify mergify bot deleted the external-prs branch March 1, 2023 11:52
@oxarbitrage oxarbitrage mentioned this pull request Mar 23, 2023
Merged
36 tasks
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@upbqdn upbqdn upbqdn approved these changes

Assignees

@teor2345 teor2345

Labels
A-devops Area: Pipelines, CI/CD and Dockerfiles A-docs Area: Documentation C-enhancement Category: This is an improvement C-trivial Category: A trivial change that is not worth mentioning in the CHANGELOG
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
2 participants
@teor2345 @upbqdn