vscode-tlaplus icon indicating copy to clipboard operation
vscode-tlaplus copied to clipboard

Using the extension with remote-ssh

Open nano-o opened this issue 2 years ago • 2 comments

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?

nano-o avatar Aug 11 '23 23:08 nano-o

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

lemmy avatar Aug 11 '23 23:08 lemmy