VScode extension error

Stream: lean4

[Adam Topaz]

I just got the following error when opening a project in vscode:

Internal error (while activating Lean 4 features):

Error: command 'lean4.restartFile' already exists
    at h.registerCommand (/opt/visual-studio-code/resources/app/out/vs/workbench/api/node/extensionHostProcess.js:153:199082)
    at Object.registerCommand (/opt/visual-studio-code/resources/app/out/vs/workbench/api/node/extensionHostProcess.js:163:21945)
    at new t.LeanClientProvider (/home/adam/.vscode/extensions/leanprover.lean4-0.0.167/dist/extension.js:1:257630)
    at /home/adam/.vscode/extensions/leanprover.lean4-0.0.167/dist/extension.js:1:192866
    at Generator.next (<anonymous>)
    at s (/home/adam/.vscode/extensions/leanprover.lean4-0.0.167/dist/extension.js:1:191621)
    at process.processTicksAndRejections (node:internal/process/task_queues:95:5)

Things seem to be working okay for now, but the error is a bit concerning. I don't really know whether this is something I should actually worry about.

[Marc Huisinga]

Thanks, I'll look into it. 0.0.167 now makes activation errors explicit and displays them so that we find out about them and fix them. This is probably an issue that already existed before and it is only now being made visible.

[Marc Huisinga]

I may have found the race condition that could cause this issue. A fix for it is in 0.0.168. Please let me know if you still encounter the internal error on that version.