Ali Caglayan (Apr 26 2021 at 14:43): Ali Caglayan (Apr 26 2021 at 14:43):Hi I am trying to use the About command in VScode but I don't see any output.
Ali Caglayan (Apr 26 2021 at 14:43):The Output window pops up with the dropdown set to Queries
Ali Caglayan (Apr 26 2021 at 14:44):There is also a Coq Language server log that I can veiw and things seem to be happening there
Ali Caglayan (Apr 26 2021 at 14:44):Is it possible to set up an info window like in coqide?
Paolo Giarrusso (Apr 26 2021 at 14:45):Might be because of a bug on first use
Paolo Giarrusso (Apr 26 2021 at 14:46):I often have to either type About by hand, or change pane to the "error" pane
Paolo Giarrusso (Apr 26 2021 at 14:47):not from Queries to Coq LS, but from the other panes on the side
Théo Winterhalter (Apr 26 2021 at 14:47):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.
Ali Caglayan (Apr 26 2021 at 17:00):Yes this is because of first use
Ali Caglayan (Apr 26 2021 at 17:00):restarting has fixed everything
Last updated: Sep 28 2023 at 11:01 UTC