mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-23 19:54:50 +03:00
11 lines
368 B
Markdown
11 lines
368 B
Markdown
# Description
|
|
|
|
|
|
## Should this change go in the CHANGELOG?
|
|
|
|
<!-- Please delete this section if it doesn't apply -->
|
|
- [ ] If this is a fix, user-facing change, a compiler change, or a new paper
|
|
implementation, I have updated [`CHANGELOG_NEXT.md`](https://github.com/idris-lang/Idris2/blob/main/CHANGELOG_NEXT.md) (and potentially also
|
|
`CONTRIBUTORS.md`).
|
|
|