diff options
| author | Fabian Mastenbroek <fabianishere@outlook.com> | 2018-07-17 16:20:47 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-07-17 16:20:47 +0200 |
| commit | 28974348022dc7c339359ffb099ec55d2c76e457 (patch) | |
| tree | a5b6c16f28dc803f3a2e6269b79e98c4e4881a96 /opendc-core/src/main | |
| parent | ebd8c8ee83704605241edf08c22df3562f52e689 (diff) | |
bug: Fix crashed processes from being resumed (#28)
This change fixes a bug where a process would be resumed again after it
had crashed, bringing down the kernel.
Fixes #27
Diffstat (limited to 'opendc-core/src/main')
0 files changed, 0 insertions, 0 deletions