Skip to content

DUX-5109 Avoid stderr get_buffer busy-loop#443

Merged
9999years merged 1 commit into
mainfrom
wiggles/dux-5109/uzwv
Apr 28, 2026
Merged

DUX-5109 Avoid stderr get_buffer busy-loop#443
9999years merged 1 commit into
mainfrom
wiggles/dux-5109/uzwv

Conversation

@9999years
Copy link
Copy Markdown
Member

If next_line() returns None in under 50ms (which happens if the stream has been closed, e.g. because the ghci process died), we busy-loop forever! There should be a break; here.

@linear
Copy link
Copy Markdown

linear Bot commented Apr 28, 2026

@9999years 9999years marked this pull request as ready for review April 28, 2026 20:05
@9999years 9999years requested a review from a team as a code owner April 28, 2026 20:05
@9999years 9999years enabled auto-merge (squash) April 28, 2026 20:05
If `next_line()` returns `None` in under 50ms (which happens if the
stream has been closed, e.g. because the `ghci` process died), we
busy-loop forever! There should be a `break;` here.
@9999years 9999years force-pushed the wiggles/dux-5109/uzwv branch from a00b53d to 40ce92a Compare April 28, 2026 21:36
@9999years 9999years requested review from dtpowl and removed request for hdgarrood April 28, 2026 21:48
@9999years 9999years merged commit dfaffa8 into main Apr 28, 2026
39 checks passed
@9999years 9999years deleted the wiggles/dux-5109/uzwv branch April 28, 2026 21:51
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