-
Notifications
You must be signed in to change notification settings - Fork 10
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
Activate extension on language 'idris2' too #91
Comments
Just adding the the language activation of idris2 is actually not enough to get the extension to work with files marked as |
Hi, it should activate anything that ends in |
Sorry, I haven't stated the problem clearly. Your extension's language definition in
The one of the LSP package.json:
|
Apologies if I've misunderstood, but for the purposes of this extension, it doesn't matter if I call the 'language', in the vscode sense, idris or idris2. Both map to the same language-configuration.json and textmate grammar. I guess it does matter in terms of the extension tags. If you search for Idris 2, this one doesn't come up, even though it does support it. |
The support of the VS Code language |
Cool, that makes sense. I want to test it when I have a chance (hopefully this weekend) and then I'll see about merging it. |
Hi,
would it be a problem if you automatically activate the extension on Idris 2 files too?
That means adding
to
package.json
.If you want to, I could generate a pull request for that.
The text was updated successfully, but these errors were encountered: