Eugene Yokota 86342d0bdd server is now called shell ...

server command is renamed to shell,
and the old shell command is called oldshell.

2017-04-14 16:35:54 -04:00

..

src/main

server is now called shell

2017-04-14 16:35:54 -04:00