| commit | a741b119e6d29061a4fbdedf35dc196e4cee67ec | [log] [tgz] |
|---|---|---|
| author | Nico Weber <nicolasweber@gmx.de> | Wed Apr 04 21:50:36 2018 -0400 |
| committer | GitHub <noreply@github.com> | Wed Apr 04 21:50:36 2018 -0400 |
| tree | 2dab6dd869df910231c866cfe1f9458d42004d36 | |
| parent | 4fd758a81bece5bc03bdb40c81de6886a06baa77 [diff] | |
| parent | b4b283e7dc43f8b29f80b37a24f1f21ddf8640c6 [diff] |
Merge pull request #1386 from jmgao/exit Don't clean up after ourselves when exiting.