exercism / idris

Exercism exercises in Idris.
https://exercism.org/tracks/idris
MIT License
32 stars 18 forks source link

Migrate existing exercises to idris2 #133

Closed isberg closed 4 months ago

github-actions[bot] commented 4 months ago

Hello. Thanks for opening a PR on Exercism 🙂

We ask that all changes to Exercism are discussed on our Community Forum before being opened on GitHub. To enforce this, we automatically close all PRs that are submitted. That doesn't mean your PR is rejected but that we want the initial discussion about it to happen on our forum where a wide range of key contributors across the Exercism ecosystem can weigh in.

You can use this link to copy this into a new topic on the forum. If we decide the PR is appropriate, we'll reopen it and continue with it, so please don't delete your local branch.

If you're interested in learning more about this auto-responder, please read this blog post.


Note: If this PR has been pre-approved, please link back to this PR on the forum thread and a maintainer or staff member will reopen it.

ErikSchierboom commented 4 months ago

I can't seem to reopen the PR. Did you maybe remove the branch?

isberg commented 4 months ago

I saw that allow edits by maintainers where not checked, so I tried checking that. If that doesn't work, I will recreate it. I guess it could be because I updated the branch, which cannot be seen in this PR.

isberg commented 4 months ago

Created a new one. https://github.com/exercism/idris/pull/134