Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Using the extension with remote-ssh #300

Open
nano-o opened this issue Aug 11, 2023 · 1 comment
Open

Using the extension with remote-ssh #300

nano-o opened this issue Aug 11, 2023 · 1 comment

Comments

@nano-o
Copy link

nano-o commented Aug 11, 2023

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?

@lemmy
Copy link
Member

lemmy commented Aug 11, 2023

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

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Development

No branches or pull requests

2 participants