search

lampepfl / dotty-feature-requests

Historical feature requests. Please create new feature requests at https://github.com/lampepfl/dotty/discussions/new?category=feature-requests
31 stars 2 forks source link

chore: add in an archive note #356

Closed ckipp01 closed 1 year ago

ckipp01 commented 1 year ago

I'm still working on sorting through the issues to transfer stuff, so we shouldn't merge this yet. However, the idea would be to get all the relevant issues transferred over to the feature requests discussions in Dotty, and then archive this repo.

ckipp01 commented 1 year ago

Alright, I think this can probably be done now. I've taken any feature request that was either created or had an active comment newer than 2020 and transferred it to the dotty discussions under feature request. I've also update the docs here to reference the new place to create a feature request. These should probably be merged together.