Skip to content
This repository has been archived by the owner on Apr 4, 2024. It is now read-only.

Add merge as an alias for r+ #746

Merged
merged 1 commit into from Oct 6, 2019
Merged

Add merge as an alias for r+ #746

merged 1 commit into from Oct 6, 2019

Conversation

DilumAluthge
Copy link
Contributor

This pull request implements the following RFC: Allow merge as an alias for r+

Specifically, this pull request adds the following aliases:

Alias added in this PR Existing command
bors merge bors r+
bors merge=FOO bors r=FOO
bors merge p=123 bors r+ p=123
bors merge=FOO p=123 bors r=FOO p=123
bors merge- bors r-

This pull request adds the following aliases:
`bors merge` -> `bors r+`
`bors merge=FOO` -> `bors r=FOO`
`bors merge p=123` -> `bors r+ p=123`
`bors merge=FOO p=123` -> `bors r=FOO p=123`
`bors merge-` -> `bors r-`
@DilumAluthge
Copy link
Contributor Author

DilumAluthge commented Oct 6, 2019

@notriddle Now that https://forum.bors.tech/t/allow-merge-as-an-alias-for-r/376 has been accepted, shall we merge this PR?

@notriddle
Copy link
Member

Agreed.

bors r+

bors bot added a commit that referenced this pull request Oct 6, 2019
746: Add `merge` as an alias for `r+` r=notriddle a=DilumAluthge

This pull request implements the following RFC: [Allow `merge` as an alias for `r+`](https://forum.bors.tech/t/allow-merge-as-an-alias-for-r/376)

Specifically, this pull request adds the following aliases:

| Alias added in this PR | Existing command |
| ---------------------- | ------------------ |
| `bors merge` | `bors r+` |
| `bors merge=FOO` | `bors r=FOO` |
| `bors merge p=123` | `bors r+ p=123` |
| `bors merge=FOO p=123` | `bors r=FOO p=123` |
| `bors merge-` | `bors r-` |

Co-authored-by: Dilum Aluthge <dilum@aluthge.com>
@bors
Copy link
Contributor

bors bot commented Oct 6, 2019

Build succeeded

@bors bors bot merged commit 00d0040 into bors-ng:master Oct 6, 2019
@DilumAluthge DilumAluthge deleted the da/bors-merge-alias branch October 6, 2019 21:58
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

2 participants