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.

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

Use Bors #84

Open
4 tasks
Indy2222 opened this issue May 24, 2022 · 2 comments
Open
4 tasks

Use Bors #84

Indy2222 opened this issue May 24, 2022 · 2 comments

Comments

@Indy2222
Copy link
Collaborator

Indy2222 commented May 24, 2022

The following conditions must be met for a PR to be merged:

  • The PR is approved by a repository administrator
  • All conversations on the PR are resolved
  • The PR is not marked as Draft
  • Rust workflow was executed successfully
@Indy2222 Indy2222 added the C-CI label May 24, 2022
@Indy2222 Indy2222 added this to the MVP milestone May 24, 2022
@Indy2222 Indy2222 removed this from the MVP milestone Nov 6, 2022
@Indy2222
Copy link
Collaborator Author

Consider using GitHub native merge queue instead.

Copy link

There is no activity on the issue for some time. The issue will be automatically closed in 3 weeks.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Development

No branches or pull requests

1 participant