diff options
| author | Dmitry Vyukov <dvyukov@google.com> | 2019-03-21 15:28:50 +0100 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-03-21 15:28:50 +0100 |
| commit | c94a70b7be6b7eb9e5f69ba547fd06f11bd4c5d4 (patch) | |
| tree | 15ee38cfb0a46546a48673ba910d6aa3a8d06dc4 /executor | |
| parent | 7c9c9fd24f0a02c137b8f438a48c2d69210bfdd1 (diff) | |
docs: add custom anchors to headers
Add shorter anchors that does not depend on actual text (subject to change).
This allows to generate shorter stable links to docs.
Let's see if this syntax works.
Diffstat (limited to 'executor')
0 files changed, 0 insertions, 0 deletions