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

[Merged by Bors] - feat(scripts/port_status): output git diff command #17630

Closed
wants to merge 2 commits into from

Conversation

ericrbg
Copy link
Collaborator

@ericrbg ericrbg commented Nov 19, 2022

We modify the port_status script to instead of listing files that have been modified, outputting the git diff command required to see the file at the current moment vs the commit that it is officially ported towards.


Open in Gitpod

We add an option (currently activated by very coarsely giving the script any input) that instead of outputting the name of modified files, outputs the `git diff` command required to see the file itself vs the commit that it is officially ported towards.
scripts/port_status.py Outdated Show resolved Hide resolved
@semorrison
Copy link
Collaborator

As Johan agrees, let's go with always outputting the git command.

bors d+

@bors
Copy link

bors bot commented Nov 23, 2022

✌️ ericrbg 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 the delegated The PR author may merge after reviewing final suggestions. label Nov 23, 2022
@ericrbg
Copy link
Collaborator Author

ericrbg commented Nov 23, 2022

bors r+

bors bot pushed a commit that referenced this pull request Nov 23, 2022
We modify the `port_status` script to instead of listing files that have been modified, outputting the `git diff` command required to see the file at the current moment vs the commit that it is officially ported towards.



Co-authored-by: Eric Rodriguez <ericrboidi@gmail.com>
@bors
Copy link

bors bot commented Nov 23, 2022

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(scripts/port_status): output git diff command [Merged by Bors] - feat(scripts/port_status): output git diff command Nov 23, 2022
@bors bors bot closed this Nov 23, 2022
@bors bors bot deleted the ericrbg-patch-1 branch November 23, 2022 15:36
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
delegated The PR author may merge after reviewing final suggestions.
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

2 participants