Stream: VsCoq devs & users

Topic: width of goal window


view this post on Zulip Yves Bertot (Feb 24 2021 at 13:11):

Hello, my goal window seem to be displaying with only a width of 10 characters. Is there a simple way to fix it?

view this post on Zulip Enrico Tassi (Feb 24 2021 at 13:20):

It's a known issue with a fix in the repo, but not released yet. The only workaround I know is to F1 and then reload extension host...

view this post on Zulip Yves Bertot (Feb 24 2021 at 13:43):

Thanks!

view this post on Zulip Théo Winterhalter (Feb 24 2021 at 13:55):

Zooming in/out solves the issue sometimes (meaning if I do it once or twice, usually it works).


Last updated: Jun 04 2023 at 23:30 UTC