From a50b9a594cc0e467bbfde0ed6465ff655e7ae821 Mon Sep 17 00:00:00 2001 From: Tony Garnock-Jones Date: Wed, 19 Feb 2014 16:42:34 -0500 Subject: [PATCH] Noddy driver for ease of repeatable runs --- drive.sh | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) create mode 100755 drive.sh diff --git a/drive.sh b/drive.sh new file mode 100755 index 0000000..1b58957 --- /dev/null +++ b/drive.sh @@ -0,0 +1,16 @@ +#!/bin/sh +racket new-server.rkt > drive-output.$(date '+%Y%m%d%H%M%S').txt 2>&1 & +serverpid=$! +echo "Serverpid is $serverpid" +while true +do + if netstat -an | grep -q '2322.*LISTEN' + then + break + fi + sleep 0.1 +done +echo '(+ 1 2 3 4 5 6)' | ssh localhost -p 2322 +sleep 1 +kill -INT $serverpid +echo "Killed $serverpid"