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.

Sign up for GitHub

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

Jump to bottom

Fix up table of library headers after all new library headers have been added #5722

Closed
tkoeppe opened this issue Aug 12, 2022 · 4 comments
Closed

Fix up table of library headers after all new library headers have been added #5722

tkoeppe opened this issue Aug 12, 2022 · 4 comments
Assignees
@tkoeppe

Comments

@tkoeppe
Copy link
Contributor

tkoeppe commented Aug 12, 2022

See comment in #5626 (comment)_
@tkoeppe tkoeppe self-assigned this Aug 12, 2022
@tkoeppe
Copy link
Contributor Author

tkoeppe commented Sep 7, 2022

I have a commit for this ready.

@jensmaurer
Copy link
Member

@tkoeppe, so please go ahead with that.

@tkoeppe
Copy link
Contributor Author

tkoeppe commented Sep 17, 2022

This has landed already, thanks!

@tkoeppe
Copy link
Contributor Author

tkoeppe commented Sep 17, 2022

Thanks -- I thought I had pressed "close with commment", must have misclicked something.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@tkoeppe tkoeppe

Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@tkoeppe @jensmaurer