Closed david-christiansen closed 7 years ago
See https://github.com/idris-lang/Idris-dev/pull/3826 for an explanation and example interaction.
It seems that the Travis script needs updating....
I need this for a demo, and I know it works.
See https://github.com/idris-lang/Idris-dev/pull/3826 for an explanation and example interaction.