Skip to content

[Merged by Bors] - feat: patch for new alias command#6172

Closed
fgdorais wants to merge 2 commits intomasterfrom
fgdorais-new-alias
Closed

[Merged by Bors] - feat: patch for new alias command#6172
fgdorais wants to merge 2 commits intomasterfrom
fgdorais-new-alias

Conversation

@fgdorais
Copy link
Copy Markdown
Collaborator

@fgdorais fgdorais commented Jul 27, 2023 •
edited
Loading

@fgdorais fgdorais mentioned this pull request Jul 27, 2023
Merged
1 task
@fgdorais fgdorais added WIP Work in progress blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) t-meta Tactics, attributes or user commands blocked-by-batt-PR This PR depends on a PR to Batteries labels Jul 27, 2023
@ghost ghost added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jul 27, 2023
@fgdorais fgdorais force-pushed the fgdorais-new-alias branch 2 times, most recently from 62531e7 to add834a Compare July 27, 2023 15:15
@fgdorais fgdorais removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Jul 27, 2023
@ghost ghost added blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) and removed merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) labels Jul 27, 2023
@fgdorais
Copy link
Copy Markdown
Collaborator Author

fgdorais commented Jul 27, 2023

This is a huge PR because it reflects a change in notation for the alias command. The first commit deals with removing the old command and the second, the huge one, changes the notation for all old alias commands. Because of its nature, this PR will systematically have merge conflicts up until the end...

@ghost ghost added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jul 28, 2023
@fgdorais fgdorais force-pushed the fgdorais-new-alias branch from add834a to cf0d910 Compare July 28, 2023 03:44
@ghost ghost added merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) and removed merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) labels Jul 28, 2023
@kbuzzard
Copy link
Copy Markdown
Member

kbuzzard commented Jul 31, 2023

For me this change is very welcome: I'd seen these alias commands before with the funny arrows and never really knew what they did; now it's absolutely clear without having to look anything up.

@fgdorais fgdorais force-pushed the fgdorais-new-alias branch from cf0d910 to 2a59618 Compare August 7, 2023 16:59
@ghost ghost removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Aug 22, 2023
@ghost
Copy link
Copy Markdown

ghost commented Aug 22, 2023

This PR/issue depends on:

@fgdorais fgdorais force-pushed the fgdorais-new-alias branch from 2a59618 to 8d2f1ec Compare August 22, 2023 11:38
@fgdorais
Copy link
Copy Markdown
Collaborator Author

fgdorais commented Aug 22, 2023

@semorrison I just updated this patch. Roll it into #6721 once it passes CI.

@ghost ghost removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Aug 22, 2023
@fgdorais fgdorais added awaiting-review and removed WIP Work in progress blocked-by-batt-PR This PR depends on a PR to Batteries labels Aug 22, 2023
@kim-em
Copy link
Copy Markdown
Contributor

kim-em commented Aug 23, 2023

Please merge or rebase after #6721 lands, and then send to bors!

bors d+

@bors
Copy link
Copy Markdown

bors bot commented Aug 23, 2023

✌️ fgdorais can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

@github-actions github-actions bot added delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). and removed awaiting-review labels Aug 23, 2023
@fgdorais
Copy link
Copy Markdown
Collaborator Author

fgdorais commented Aug 23, 2023

bors r+

@bors
Copy link
Copy Markdown

bors bot commented Aug 23, 2023

Merge conflict.

@fgdorais fgdorais force-pushed the fgdorais-new-alias branch 2 times, most recently from 3fda6de to 74afc31 Compare August 23, 2023 02:58
@fgdorais
Copy link
Copy Markdown
Collaborator Author

fgdorais commented Aug 23, 2023

bors try

bors bot added a commit that referenced this pull request Aug 23, 2023
@bors
Try #6172:
9fc7d22
@bors
Copy link
Copy Markdown

bors bot commented Aug 23, 2023

try

Build failed:

@fgdorais fgdorais force-pushed the fgdorais-new-alias branch from 74afc31 to fa9e7aa Compare August 23, 2023 03:46
@fgdorais
Copy link
Copy Markdown
Collaborator Author

fgdorais commented Aug 23, 2023

bors try

bors bot added a commit that referenced this pull request Aug 23, 2023
@bors
Try #6172:
226fb02
@bors
Copy link
Copy Markdown

bors bot commented Aug 23, 2023

try

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

@fgdorais
Copy link
Copy Markdown
Collaborator Author

fgdorais commented Aug 23, 2023

bors merge

bors bot pushed a commit that referenced this pull request Aug 23, 2023
@fgdorais
feat: patch for new alias command (#6172)
19e0ba9
@bors
Copy link
Copy Markdown

bors bot commented Aug 23, 2023

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

@bors bors bot changed the title feat: patch for new alias command [Merged by Bors] - feat: patch for new alias command Aug 23, 2023
@bors bors bot closed this Aug 23, 2023
@bors bors bot deleted the fgdorais-new-alias branch August 23, 2023 04:39
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). t-meta Tactics, attributes or user commands

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@fgdorais @kbuzzard @kim-em