finish up for merge

This commit is contained in:
Johann150 2021-03-23 23:25:04 +01:00
parent 782e043083
commit eec057515d
No known key found for this signature in database
GPG key ID: 9EE6577A2A06F8F1
3 changed files with 9 additions and 5 deletions

View file

@ -81,8 +81,7 @@ impl Drop for Server {
// a potential error message was not yet handled
self.stop().unwrap();
} else if self.output.is_some() {
// error was already handled, ignore it
self.stop().unwrap_or(());
// server was already stopped
} else {
// we are panicking and a potential error was not handled
self.stop().unwrap_or_else(|e| eprintln!("{:?}", e));