vscode-tlaplus
vscode-tlaplus copied to clipboard
Using the extension with remote-ssh
Hello, it seems that the extension does not work when accessing a remote folder using SSH (with the SSH extension from Microsoft). VSCode says the extension is defined to run in the remote host and that it is not installed in the remote host; but it is installed on the remote host. Am I missing something, or is this just not supposed to work?
I've never tried this and don't know how this is supposed to work, but the extension simply spawns a TLC process https://github.com/tlaplus/vscode-tlaplus/blob/4a0d7233df210ebada17ba2252da7a6b14560c3d/src/tla2tools.ts#L132C24-L146