Commit 80d5f1347d70550d49d95b6420ca27877d1221e8

Stefan Sperling 2018-11-11T12:59:22

don't be noisy on stderr when Ctrl-C is hit