Revert the --restart -> --restart_server rename

This commit is contained in:
Ondřej Surý
2020-05-01 14:01:47 +02:00
parent adb73b1fc0
commit 3127e7680e
6 changed files with 13 additions and 13 deletions

View File

@@ -80,7 +80,7 @@ stomp () {
restart () {
sleep 1
start_server --noclean --restart_server --port "${PORT}" masterformat ns3
start_server --noclean --restart --port "${PORT}" masterformat ns3
}
dig_with_opts() {