You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
The extension doesn't work in the github.dev web editor: "The 'TLA+' extension is not available in Visual Studio Code for the Web."
Why is an extension not installable in the browser#
There are a small number of extensions that have built-in assumptions or need to run on the desktop. Examples are when an extension accesses files from the VS Code installation on the desktop or when an extension depends on an executable that must run in a desktop environment. When you try to install such an extension in the browser, you will be informed that the extension is not available.
Notice such an extension can still be used when connecting to a Codespace from VS Code running on the desktop.
The extension doesn't work in the github.dev web editor: "The 'TLA+' extension is not available in Visual Studio Code for the Web."
(from https://code.visualstudio.com/docs/remote/codespaces#_why-is-an-extension-not-installable-in-the-browser) Also, https://code.visualstudio.com/updates/v1_60#_web-extensions has technical background.
It is unlikely that TLC will ever run in the browser, but syntax highlighting should be possible.
The text was updated successfully, but these errors were encountered: