From 190663a2531d52ac2e3f45f61c1166455bcaba1e Mon Sep 17 00:00:00 2001
From: Midgard <midgard@zeus.ugent.be>
Date: Wed, 25 Mar 2020 22:28:22 +0100
Subject: [PATCH] Improve rundev script

Kill server when exiting MITM
---
 rundev.sh | 13 ++++++++++++-
 1 file changed, 12 insertions(+), 1 deletion(-)

diff --git a/rundev.sh b/rundev.sh
index ab896d3..71daa64 100755
--- a/rundev.sh
+++ b/rundev.sh
@@ -1,14 +1,25 @@
 #!/bin/bash
 
+
+# Config
 MATTERMOST_REMOTE="https://mattermost.zeus.gent"
 
 
+
+set -euo pipefail
+
+cd "$(dirname "$0")"
 if [[ $MATTERMOST_REMOTE == */ ]]; then
 	echo "MATTERMOST_REMOTE should not end with a slash (it should only the protocol and the domain; no path)" >&2
 	exit 1
 fi
 
-cd "$(dirname "$0")"
+server_pid=0
+finish() {
+	if [[ $server_pid -gt 1 ]]; then kill "$server_pid" || true; server_pid=0; fi
+}
+trap finish EXIT
 
 python3 -m "http.server" >/dev/null 2>&1 &
+server_pid=$!
 mitmproxy -s etc/mitm_cors.py -m "reverse:$MATTERMOST_REMOTE"