kill server when port is already used demo
authorAnthony Garcia <anthony.garcia@inria.fr>
Mon, 30 Sep 2013 10:55:32 +0000 (12:55 +0200)
committerAnthony Garcia <anthony.garcia@inria.fr>
Mon, 30 Sep 2013 10:55:32 +0000 (12:55 +0200)
commit31f84d68d3bd9208a91abc1f2f59389e1a0caca3
treea85c09fa528596a91928eebdb1178f99ff739e34
parentaed0ffdc0b0cad9bc2175f718249a6fa4f7d7158
kill server when port is already used
devel/server-loop.sh