Closed ejgallego closed 6 months ago
New trim command (both in the server and in VSCode) to liberate space used in the cache.
Command available as
Coq LSP: Request the server to trim caches and compact memory
Fixes #367
cc: #253 #236 #348 , which may be greatly alleviated by this PR.
New trim command (both in the server and in VSCode) to liberate space used in the cache.
Command available as
Coq LSP: Request the server to trim caches and compact memory
Fixes #367
cc: #253 #236 #348 , which may be greatly alleviated by this PR.