[Merged by Bors] - chore: script to replace headers with #align_import statements#5979
[Merged by Bors] - chore: script to replace headers with #align_import statements#5979
Conversation
|
This PR/issue depends on:
|
| #!/usr/bin/env python3 | ||
|
|
||
| # This script was written by ChatGPT. | ||
| # https://chat.openai.com/share/e0363ebf-ed6f-4fd8-9b76-ebf422ed9f62 |
There was a problem hiding this comment.
This should include a doc-comment along the lines of:
"""
This script was used in #5979 to convert from one header format to another.
It can be safely deleted in a few weeks.
"""There was a problem hiding this comment.
Or we could just delete it and not ever commit it; it's only use is being in the history for this PR, really.
eric-wieser
left a comment
There was a problem hiding this comment.
bors d+
Some downstream stuff will break, and I won't be fixing it for at least 8 hours.
Merging in 6 hours or so is probably a good compromise, since it might take some time to propagate anyway.
|
✌️ semorrison can now approve this pull request. To approve and merge a pull request, simply reply with |
|
Thanks 🎉 bors merge |
- [x] depends on: #5966 [](https://gitpod.io/from-referrer/) Co-authored-by: Eric Wieser <wieser.eric@gmail.com> Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
|
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. If you want to switch to GitHub's built-in merge queue, visit their help page. |
- [x] depends on: #5966 [](https://gitpod.io/from-referrer/) Co-authored-by: Eric Wieser <wieser.eric@gmail.com> Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
align_importcommand #5966