scripts/: some useful bash scripts to launch the server and do port forwarding 39e8fd5 Marti Umbert commited on Apr 17
