Closed ghost closed 3 years ago
Thanks for the PR, very much appreciated.
The tests appear to fail with:
In toplevel form:
idris-commands.el:765:19:Error: assignment to free variable `def-region-start'
I am wondering if you can have a look at that.
Thanks!
Thanks for the PR, very much appreciated.
The tests appear to fail with:
In toplevel form: idris-commands.el:765:19:Error: assignment to free variable `def-region-start'
I am wondering if you can have a look at that.
Thanks!
It should be fixed now.
Thanks! Most of the builds ran to completion! The last two failed due to what looks like external factors.
I have restarted the failing builds to see what happens.
Can we also get the changelog updated as well?
Thanks
I am very sorry that this PR has been the 'p' and 'r' in purgatory. Having started on some revision of the mode to accommodate breaking changes to the IDE protocol in Idris2, I saw that I missed the follow up to this. I've merged now. Very sorry about this.
Idris2 has two new IDE commands generate-def and generate-def-next.