aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorJohn MacFarlane <jgm@berkeley.edu>2019-04-08 12:36:32 -0700
committerJohn MacFarlane <jgm@berkeley.edu>2019-04-08 12:36:32 -0700
commite3317c5ea38f4b4580dbb08a1be06d17110a6b6c (patch)
treea49253e072ab47bcc1dd7af2e42dca4be14f7417
parentecc839773e948377d83799a525e81fcf81badc65 (diff)
Adopt make_spec.lua for lua 5.3 and new number type.
So we don't get `<h2.0>`.
-rw-r--r--tools/make_spec.lua2
1 files changed, 1 insertions, 1 deletions
diff --git a/tools/make_spec.lua b/tools/make_spec.lua
index acfdb61..144a5af 100644
--- a/tools/make_spec.lua
+++ b/tools/make_spec.lua
@@ -156,7 +156,7 @@ local create_anchors = function(doc, meta, to)
stop="}\\label{" .. ident .. "}}",
block = true})
else
- anchor = make_html_block('h' .. tostring(level),
+ anchor = make_html_block('h' .. tostring(math.floor(level)),
{{'id', ident},
{'href', '#'..ident},
{'class', 'definition'}})