Skip to content

Update for latest idris#18

Open
beefyhalo wants to merge 1 commit intoedwinb:masterfrom
beefyhalo:master
Open

Update for latest idris#18
beefyhalo wants to merge 1 commit intoedwinb:masterfrom
beefyhalo:master

Conversation

@beefyhalo
Copy link

Fixes the build :)

Copy link

@smeden-lod smeden-lod left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

great fix !

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants

Comments