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

[utilities] review of library index #855

Closed
wants to merge 1 commit into from

Conversation

AlisdairM
Copy link
Contributor

This review handles several topic related to the index
of library names:
fix outright errors, indexing the wrong name
fix errors of omission: every itemdecl is now indexed
consistent ordering of indexlibrarymember{identifier}{class-name}
every index macro has a trailing % to avoid accidental whitespace
all headers have an idxhdr entry

This review handles several topic related to the index
of library names:
  fix outright errors, indexing the wrong name
  fix errors of omission: every itemdecl is now indexed
  consistent ordering of indexlibrarymember{identifier}{class-name}
  every index macro has a trailing % to avoid accidental whitespace
  all headers have an indexhdr entry
@AlisdairM
Copy link
Contributor Author

Amended commit with the last few \indexlibrarymember uses that were {class}{identifier} rather than the other way around.

@tkoeppe
Copy link
Contributor

tkoeppe commented Jul 26, 2016

See #861

@tkoeppe tkoeppe closed this Jul 26, 2016
@AlisdairM AlisdairM deleted the index_review_clause_20 branch August 8, 2016 14:17
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

2 participants