idris-mode icon indicating copy to clipboard operation
idris-mode copied to clipboard

Published 20 hours ago • verified publisher icon idris-hackers

Merge idris2-mode back into idris-mode

Open gallais opened this issue 3 years ago • 2 comments

Let's see how this goes.

gallais avatar Dec 02 '21 14:12 gallais

This is interesting...

jfdm avatar Dec 07 '21 16:12 jfdm

I gave up the idea of cherry-picking as that still leaves merge conflicts. Instead I am going full merge here: https://github.com/gallais/idris2-mode/pull/1

It's not passing the tests yet but it's not too far from being a working mode.

gallais avatar Dec 07 '21 16:12 gallais