Hi I am trying to use the About command in VScode but I don't see any output.
The Output window pops up with the dropdown set to Queries
There is also a Coq Language server log that I can veiw and things seem to be happening there
Is it possible to set up an info window like in coqide?
Might be because of a bug on first use
I often have to either type About by hand, or change pane to the "error" pane
not from Queries to Coq LS, but from the other panes on the side
For me at least
Prompt About works. But sometimes the output is not shown and I have to close the pane and do it again.
Yes this is because of first use
restarting has fixed everything
Last updated: Jan 30 2023 at 17:03 UTC