Shreyas Srinivas (May 10 2023 at 16:12): Shreyas Srinivas (May 10 2023 at 16:12):I opened vscode via isabelle vscode (Linux). This opened up the vscodium bundled with vscode with the isabelle extension but nothing else. Is there a simple way to import most or all of my existing vscode extensions?
Shreyas Srinivas (May 10 2023 at 16:24):The standard Vscodium solution of copying vscode extensions folder requires me to know where the extension folder actually is for isabelle's vscodium
Last updated: Apr 28 2024 at 04:17 UTC