Idris2 icon indicating copy to clipboard operation
Idris2 copied to clipboard

Published 20 hours ago • verified publisher icon idris-lang

Trans deps v3

Open Z-snails opened this issue 3 years ago • 5 comments

See #2496 and #2469 pinging @stefan-hoeck

Z-snails avatar Jul 10 '22 09:07 Z-snails

Thanks for reopening this. And sorry, seems I forgot to adjust the error messages from the pkg006 test.

stefan-hoeck avatar Jul 10 '22 15:07 stefan-hoeck

Just for your info, I tested this against the pack collection without any issues (I know we had that before, but it's still good to know everything went well).

stefan-hoeck avatar Jul 10 '22 17:07 stefan-hoeck

@Z-snails : Any news on this? Once the expected result of the failing idris2/pkg006 test has been adjusted, this should be ready for revision.

stefan-hoeck avatar Jul 27 '22 14:07 stefan-hoeck

I'm currently on holiday, so for the next few days I'm unable to do basically anything other than comment or merge, so I'm more than happy to leave this to you (although if it's my fork this PR is from that might be trickier, but if anything needs fixing I'll merge a PR to my fork)

Z-snails avatar Jul 27 '22 17:07 Z-snails

@Z-snails I submitted a PR to your fork with the test pkg006 fixed.

stefan-hoeck avatar Aug 04 '22 14:08 stefan-hoeck