Julio Di Egidio

LSP plugin mangling VSCode/ium Settings file

2

### **Describe the bug** Upon activation, the **plugin** adds entries to the ".vscode/settings.json" file, which represents Workspace Settings, or creates the file if it does not exist already. Specifically, the...

### Description of the problem Coqdoc's output.ml generates HTML anchors associated to section titles that are simply useless at the moment. See: https://github.com/coq/coq/blob/master/tools/coqdoc/output.ml#L833 Of course, these direct links are quite...