From c68cf4de2598542d359f8fe208b9674167d94f9d Mon Sep 17 00:00:00 2001 From: Justus Springer Date: Wed, 22 Apr 2026 14:37:55 +0100 Subject: [PATCH] fix guard in mk_tooltip --- lua/lean/widget/interactive_code.lua | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lua/lean/widget/interactive_code.lua b/lua/lean/widget/interactive_code.lua index b3dae4ef..2bce87df 100644 --- a/lua/lean/widget/interactive_code.lua +++ b/lua/lean/widget/interactive_code.lua @@ -64,7 +64,7 @@ local function render_subexpr_info(subexpr_info, tag, sess, locations, self_rend tooltip_element:add_child(InteractiveCode(info_popup.type, sess, locations)) end - if info_popup.doc ~= nil then + if type(info_popup.doc) == 'string' then tooltip_element:add_child(Element:new { text = '\n\n' }) tooltip_element:add_child(Element:new { text = info_popup.doc }) -- TODO: markdown end