On Tue, 1 Mar 2022, Stuart Henderson wrote:
I suggest doing this as a separate port.
That was my first intention but somehow I thought it would be easer to mantain keeping it in the same port. If you (the developers, specially the arm ones) think this is better I could write another port when I have some time. Some advise about the distfile? Should I stick to the same version?
