diff options
| author | Damien George <damien.p.george@gmail.com> | 2018-05-31 23:11:08 +1000 |
|---|---|---|
| committer | Damien George <damien.p.george@gmail.com> | 2018-06-12 11:56:25 +1000 |
| commit | b2fa1b50edaea43007d692d24391c6f3aa4d15ca (patch) | |
| tree | a048c894df68b3db11ca6140aed6ec79fae5795e /ports/unix | |
| parent | 522ea80f06a80fd799bd57de351373ceaeeae325 (diff) | |
ports: Call gc_sweep_all() when doing a soft reset.
This calls finalisers of things like files and sockets to cleanly close
them.
Diffstat (limited to 'ports/unix')
| -rw-r--r-- | ports/unix/main.c | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/ports/unix/main.c b/ports/unix/main.c index b68fe9279..1cf237a2b 100644 --- a/ports/unix/main.c +++ b/ports/unix/main.c @@ -647,6 +647,10 @@ MP_NOINLINE int main_(int argc, char **argv) { } #endif + #if defined(MICROPY_UNIX_COVERAGE) + gc_sweep_all(); + #endif + mp_deinit(); #if MICROPY_ENABLE_GC && !defined(NDEBUG) |