meraymond2 / idris-vscode

Idris front-end for VS Code
MIT License
58 stars 10 forks source link

"Idris 2 mode" checkbox is missing #77

Closed srid closed 2 years ago

srid commented 2 years ago

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 commented 2 years ago

PEBKAC !

Had the wrong extension installed