diff options
| author | Christoph Päper <bugzilla@crissov.de> | 2019-12-16 21:48:15 +0100 |
|---|---|---|
| committer | John MacFarlane <jgm@berkeley.edu> | 2019-12-16 12:48:15 -0800 |
| commit | e4618d1f3db70710b81b77e0fe98a734d6c90c06 (patch) | |
| tree | f09fa11ed96d800453a3c2e5cc3d61f9db3f618b | |
| parent | 613a9afbb96b7868c56cf9bf9cf94d357baf9630 (diff) | |
Update make_spec.lua (#626)
Removes extraneous href attribute on headings.
fixes #625
| -rw-r--r-- | tools/make_spec.lua | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/tools/make_spec.lua b/tools/make_spec.lua index 05a1270..c247142 100644 --- a/tools/make_spec.lua +++ b/tools/make_spec.lua @@ -168,7 +168,6 @@ local create_anchors = function(doc, meta, to) else anchor = make_html_block('h' .. tostring(math.floor(level)), {{'id', ident}, - {'href', '#'..ident}, {'class', 'definition'}}) if num ~= '' then local numspan = make_html_inline('span', {{'class','number'}}) |