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] - ci: add a workflow to detect SHA changes in header comments #2255

Closed
wants to merge 4 commits into from

Conversation

eric-wieser
Copy link
Member

@eric-wieser eric-wieser commented Feb 13, 2023

This looks over the diff in a PR, and detects any changes to header comments. When it finds them, it

  • generates links to help review forward-ports
  • ensures that invalid header comments don't get inserted.

Open in Gitpod

A demo can be seen at #2257

@eric-wieser eric-wieser marked this pull request as ready for review February 13, 2023 14:56
@eric-wieser eric-wieser added the WIP Work in progress label Feb 13, 2023
@eric-wieser eric-wieser changed the title Add sha change comments ci: add a workflow to detect SHA changes in header comments Feb 13, 2023
@eric-wieser eric-wieser added enhancement New feature or request awaiting-review and removed WIP Work in progress labels Feb 13, 2023
@jcommelin
Copy link
Member

Thanks 🎉

bors merge

@github-actions github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Feb 13, 2023
bors bot pushed a commit that referenced this pull request Feb 13, 2023
This looks over the diff in a PR, and detects any changes to header comments. When it finds them, it
* generates links to help review forward-ports
* ensures that invalid header comments don't get inserted.
@bors
Copy link

bors bot commented Feb 13, 2023

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title ci: add a workflow to detect SHA changes in header comments [Merged by Bors] - ci: add a workflow to detect SHA changes in header comments Feb 13, 2023
@bors bors bot closed this Feb 13, 2023
@bors bors bot deleted the add-sha-change-comments branch February 13, 2023 19:08
mo271 pushed a commit that referenced this pull request Feb 18, 2023
This looks over the diff in a PR, and detects any changes to header comments. When it finds them, it
* generates links to help review forward-ports
* ensures that invalid header comments don't get inserted.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
enhancement New feature or request ready-to-merge This PR has been sent to bors.
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

2 participants