Allow docker scripts to be run from other directories

docker/build-docker

@@ -1,4 +1,9 @@
 #!/bin/bash
 
+# cd into the directory containing this script (from the bash faq 028)
+if [[ $BASH_SOURCE = */* ]]; then
+  cd -- "${BASH_SOURCE%/*}/" || exit
+fi
+
 cd ..
 docker build $* -t prac -f docker/Dockerfile .

docker/set-networking

@@ -1,5 +1,10 @@
 #!/bin/bash
 
+# cd into the directory containing this script (from the bash faq 028)
+if [[ $BASH_SOURCE = */* ]]; then
+  cd -- "${BASH_SOURCE%/*}/" || exit
+fi
+
 latency=30ms
 bw=100mbit