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

Update `System::refresh_processes` API to give control over when to remove dead processes #1353

Merged

GuillaumeGomez merged 1 commit into master from rm-dead-processes

Oct 3, 2024

Owner

GuillaumeGomez commented Oct 3, 2024

Fixes #1340.

GuillaumeGomez force-pushed the rm-dead-processes branch 5 times, most recently from 5a8928b to bc9fc75 Compare

October 3, 2024 21:37


          Update System::refresh_processes API to give control over when to r…

7452b8d

…emove dead processes

GuillaumeGomez force-pushed the rm-dead-processes branch from bc9fc75 to 7452b8d Compare

October 3, 2024 21:49

GuillaumeGomez merged commit 2fb2903 into master

66 of 67 checks passed

GuillaumeGomez deleted the rm-dead-processes branch

October 3, 2024 22:01

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

Labels

None yet