Tools: properly handle the keyboard interrupt#2083

Merged

yonghong-song merged 1 commit intoiovisor:masterfrom jeromemarchand:ctrl-c

Dec 19, 2018

Commits on Dec 17, 2018

Tools: properly handle the keyboard interrupt
jeromemarchand
committed