search

madman-bob / idris2-python

A Python backed for Idris 2
Other
19 stars 4 forks source link

Fix compilation error with latest Idris2 #3

Closed gwerbin closed 2 years ago

gwerbin commented 2 years ago

Apparently an appendFile function was added to System.File in Idris 2, resulting in a name conflict and compilation error. Using the fully-qualified name fixes it.

madman-bob commented 2 years ago

Resolved instead by removing our version of appendFile, as the behaviours are the same.