On Thu, 22 Apr 2021 10:39:53 +0200
Xinglu Chen <public@yoctocell.xyz> wrote:

> I think you forgot the attach the patch. ;)
> 

Ah heck. That might have been the case.
Here it is.

There hasn't been a tagged release since then, so I'm sending my
original patch, but I should note that in my channel I've been tracking
the latest commit, which does seem to work, although it's been a while
since I used Idris for anything complicated.