It seems that https://github.com/coq/coq/tree/master/dev/doc / https://github.com/coq/coq/wiki/DevelSetup doesn't cover VSCode?

@Paolo Giarrusso please open an issue so that can be fixed in the BSP

https://github.com/coq/coq/issues/15684, pre-labeled "help wanted"

Last updated: Jan 29 2023 at 16:02 UTC