diff options
| author | Matej Kosik | 2015-10-29 10:22:37 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2015-12-10 09:35:08 +0100 |
| commit | 950dace27c3233f740b2031c9d99cb3f155aefbf (patch) | |
| tree | 08565011edd7eecf02354fa27d93c387d22d5e2c /plugins/syntax/numbers_syntax.ml | |
| parent | 0117f54f3e3678f348f8ed84c8444dc614ce8298 (diff) | |
ENH: Index anchor repositioning.
Originally, when user clicked in index on "Type", he landed
on an incorrect page (immediatelly following the page
which actually contains the definition of "Type").
Diffstat (limited to 'plugins/syntax/numbers_syntax.ml')
0 files changed, 0 insertions, 0 deletions