idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-28 22:22:10 +03:00
Code Issues Projects Releases Wiki Activity

Remove duplicate template

Browse Source
This commit is contained in:
Edwin Brady 2020-05-20 22:04:11 +01:00
parent f819c0b855
commit b2e7c40da9
1 changed files with 0 additions and 12 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

12
.github/ISSUE_TEMPLATE/large-feature-requests-and-proposals.md vendored
View File

@ -1,12 +0,0 @@
---
name: Large feature requests and proposals
about: What to do if you have a feature request or proposal
title: ''
labels: Proposal (please add to wiki/mailing list)
assignees: ''
---
Experience with Idris 1 suggests that larger feature requests and proposals tend to get buried among the bug reports in the issue tracker, even if we tag the effectively. Partly this is because there's not many people working on Idris full time (it's about half a person at the moment), but also, it's because it's not objectively clear how to resolve such issues.
So, instead, please add the details on the wiki, at https://github.com/edwinb/Idris2/wiki/Contributions-wanted, which I hope will be more discoverable. It's also a good idea to suggest it on the mailing list and/or the IRC channel, which are good places for more detailed discussion.