diff Makefile @ 33506:8a1a7935c047

commandserver: close selector explicitly The selector does not have a __del__ method and needs a manual close. We can also use "with selector" but that makes the code too indented. Therefore append a "selector.close()" after the end of the main loop for now.
author Jun Wu <quark@fb.com>
date Sun, 16 Jul 2017 04:39:32 -0700
parents 91ae09010950
children c5607b65fcb8
line wrap: on
line diff