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

"Idris 2 mode" checkbox is missing #77

Closed
srid opened this issue Dec 18, 2021 · 1 comment
Closed

"Idris 2 mode" checkbox is missing #77

srid opened this issue Dec 18, 2021 · 1 comment

Comments

@srid
Copy link

srid commented Dec 18, 2021

README says,

Currently the extension will default to v1. If you want it to use Idris 2, change the path in the configuration to your Idris 2 binary, and tick the Idris 2 Mode checkbox.

But I see no such checkbox in VSCode. This is what I see:

image

Incidentally, the extension throws an error:

image

with the Idris2 program in question being a simple:

module Main

main : IO ()
main = putStrLn "Hello world!"
@srid
Copy link
Author

srid commented Dec 18, 2021

PEBKAC !

Had the wrong extension installed

@srid srid closed this as completed Dec 18, 2021
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant