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.

Sign up for GitHub

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

Jump to bottom

progress: avoid edge-case where we try to run a dead thread #205

Merged

grosser merged 1 commit into master from grosser/pass

Oct 8, 2022

Owner

grosser commented Oct 4, 2022

t = Thread.new { }
r.run -> ThreadError (killed thread)

grosser mentioned this pull request

make progress stop when block stops #204

Merged


          progress: avoid edge-case where we try to run a dead thread

129e5c0

grosser force-pushed the grosser/pass branch from 2aca6bc to 129e5c0 Compare

October 4, 2022 18:31

grosser merged commit ef8728a into master

grosser deleted the grosser/pass branch

October 8, 2022 02:07

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet