Merge pull request #420 from rbberger/doc_anchor_check
Add utility to detect duplicate anchors in docs
GitHub <noreply@github.com> | Mar 17 2017, 18:17 |
junge | Oct 19 2017, 09:53 |
Commit | Author | Details | Committed | |||
---|---|---|---|---|---|---|
621d7d5ce0f2 | Richard Berger | Correct off-by-one error in line number reported | Mar 17 2017 | |||
1bb9c7da42e5 | Richard Berger | Remove some duplicate anchors in documentation | Mar 17 2017 | |||
f893104b18d1 | Richard Berger | Add anchor_check to doc Makefile | Mar 17 2017 | |||
efb2a942e046 | Richard Berger | Add utility to detect duplicate anchors in documentation files | Mar 17 2017 |