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

Do not exit the repl when Ctrl-C is pressed, fixes #6870 #6885

Open
wants to merge 5 commits into
base: main
Choose a base branch
from

Conversation

ageron
Copy link
Contributor

@ageron ageron commented Jul 7, 2024

Ctrl-C currently exits the REPL. In virtually every other REPL, Ctrl-C just cancels the current command, it doesn't exit. This means that users will accidently close their ROC REPL and lose their current work. It's also convenient to be able to cancel the current command very simply (without having to type Ctrl-A + Ctrl-K).

See the discussion in #6870.

@folkertdev folkertdev requested a review from rtfeldman July 7, 2024 21:16
@ageron ageron force-pushed the ignore-ctrl-c-in-repl branch from 4538e0c to 4c43d54 Compare August 1, 2024 10:05
Copy link

github-actions bot commented Sep 1, 2024

Thank you for your contribution! Sometimes PRs end up staying open for a long time without activity, which can make the list of open PRs get long and time-consuming to review. To keep things manageable for reviewers, this bot automatically closes PRs that haven’t had activity in 60 days. This PR hasn’t had activity in 30 days, so it will be automatically closed if there is no more activity in the next 30 days. Keep in mind that PRs marked Closed are not deleted, so no matter what, the PR will still be right here in the repo. You can always access it and reopen it anytime you like!

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.

1 participant