Script to stop all three sets of dockers

This is useful if, for example, a run of repro-all-dockers is
interrupted, leaving some dockers (and potentionally the processes
therein) running.

repro/stop-all-dockers

@@ -0,0 +1,28 @@
+#!/bin/bash
+
+# Stop all three sets of dockers.  This is useful if, for example, a run
+# of repro-all-dockers is interrupted, leaving some dockers (and
+# potentionally the processes therein) running.
+
+# cd into the directory containing this script (from the bash faq 028)
+if [[ $BASH_SOURCE = */* ]]; then
+  cd -- "${BASH_SOURCE%/*}/" || exit
+fi
+
+# Duoram
+echo Stopping Duoram dockers
+echo
+( cd ../Docker && ./stop-docker ) || exit 1
+
+# Floram
+echo
+echo Stopping Floram dockers
+echo
+( cd floram-docker && ./stop-docker ) || exit 1
+
+# Circuit ORAM
+echo
+echo Stopping Circuit ORAM dockers
+echo
+( cd circuit-oram-docker/docker && ./stop-docker ) || exit 1
+