aboutsummaryrefslogtreecommitdiff
path: root/tools
diff options
context:
space:
mode:
authorChristoph Päper <bugzilla@crissov.de>2019-12-16 21:48:15 +0100
committerJohn MacFarlane <jgm@berkeley.edu>2019-12-16 12:48:15 -0800
commite4618d1f3db70710b81b77e0fe98a734d6c90c06 (patch)
treef09fa11ed96d800453a3c2e5cc3d61f9db3f618b /tools
parent613a9afbb96b7868c56cf9bf9cf94d357baf9630 (diff)
Update make_spec.lua (#626)
Removes extraneous href attribute on headings. fixes #625
Diffstat (limited to 'tools')
-rw-r--r--tools/make_spec.lua1
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'}})