Open gallais opened 2 years ago
I don't have access to idris1 & it's pretty annoying to swtich between idris-mode and idris2-mode for testing so I figured I'd ask here:
Would idris-mode benefit from a fix similar to https://github.com/idris-community/idris2-mode/pull/20 ?
I just checked: the Compile & Execute menu works for Idris1 only, Idris2 causes an error. So yes fixing Idris-mode for idris2 would be good.
I don't have access to idris1 & it's pretty annoying to swtich between idris-mode and idris2-mode for testing so I figured I'd ask here:
Would idris-mode benefit from a fix similar to https://github.com/idris-community/idris2-mode/pull/20 ?