Stop emitting intent="@ignore"

This commit is contained in:
Marcel Fabian Krüger 2024-07-17 19:36:49 +02:00
parent e74bca7eac
commit 413ec0112a

View File

@ -616,9 +616,10 @@ function nodes_to_table(head, cur_style, text_families)
end end
joining = new_joining joining = new_joining
end end
-- In TeX, groups are never space like -- In TeX, groups are never space like, so we insert an artificial node instead.
-- This node should be ignored for most purposes
if core == space_like then if core == space_like then
core = {[0] = 'mi', intent = '@ignore'} core = {[0] = 'mi', ['tex:ignore'] = 'true'}
result[#result+1] = core result[#result+1] = core
end end
if t[0] == 'mrow' and #t == 1 then if t[0] == 'mrow' and #t == 1 then