Skip to content
New issue

Have a question about this project? # for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “#”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? # to your account

[ base ] Add casts between Int and ExitCode #3432

Merged
merged 1 commit into from
Dec 2, 2024

Conversation

spcfox
Copy link
Contributor

@spcfox spcfox commented Dec 2, 2024

Description

system returns Int, and exitWith takes ExitCode. So it is useful to have casts between the two. In particular this is needed for #3427, because most code generators use system for executeExpr.

Should this change go in the CHANGELOG?

  • If this is a fix, user-facing change, a compiler change, or a new paper
    implementation, I have updated CHANGELOG_NEXT.md (and potentially also
    CONTRIBUTORS.md).

@andrevidela
Copy link
Collaborator

Thanks, this looks good

@andrevidela andrevidela merged commit 35cbbcc into idris-lang:main Dec 2, 2024
20 of 22 checks passed
andrevidela pushed a commit to andrevidela/Idris2 that referenced this pull request Dec 13, 2024
andrevidela pushed a commit to andrevidela/Idris2 that referenced this pull request Dec 17, 2024
andrevidela pushed a commit to andrevidela/Idris2 that referenced this pull request Dec 24, 2024
andrevidela pushed a commit to andrevidela/Idris2 that referenced this pull request Dec 29, 2024
# for free to join this conversation on GitHub. Already have an account? # to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants