Zulip Chat Archive
Stream: general
Topic: Error in popup for `congr'`
Stuart Presnell (Dec 23 2021 at 13:56):
In VS Code, when I mouseover the tactic congr' in the file I'm working on, the popup window shows the following error:
Screenshot-2021-12-23-at-13.44.19.png
Mario Carneiro (Dec 23 2021 at 13:59):
raahh, I can't count how many times I have seen and fixed this issue, it just won't die
Mario Carneiro (Dec 23 2021 at 14:13):
Stuart Presnell (Dec 27 2021 at 07:01):
Sorry to be the bearer of bad news, but I've just seen the same error in the popup for ext1 Screenshot-2021-12-27-at-06.59.39.png
Stuart Presnell (Dec 27 2021 at 07:02):
:ghost:
Mario Carneiro (Dec 27 2021 at 07:44):
Looks like #11004 hasn't been merged yet, so it might be fixed already and not propagated
Mario Carneiro (Dec 27 2021 at 07:45):
can confirm that the ext1 hover works on the #11004 branch
Last updated: Dec 20 2023 at 11:08 UTC