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

Create a new index for library headers #1835

Merged
merged 1 commit into from Nov 26, 2017
Merged

Create a new index for library headers #1835

merged 1 commit into from Nov 26, 2017

Conversation

jensmaurer
Copy link
Member

and remove them from the index of library names.

Fixes #1807.

@tkoeppe tkoeppe force-pushed the master branch 2 times, most recently from b97296d to 75c0adc Compare November 21, 2017 22:53
@jensmaurer
Create a new index for library headers
f9ae39e 
and remove them from the index of library names.
@jensmaurer
Copy link
Member Author

(The index is actually two pages, not one, contrary to the estimation by @zygoloid in #1807.)

The separate index seems rather useful to get an overview of all headers in the standard library. You might also want to mention it in the editor's report.

@zygoloid zygoloid merged commit bd2ce5c into cplusplus:master Nov 26, 2017
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@zygoloid zygoloid Awaiting requested review from zygoloid

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
2 participants
@jensmaurer @zygoloid