Skip to content
New issue

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

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

Already on GitHub? Sign in 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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants