Push-and-update script.

pull-and-update.sh

@@ -0,0 +1,9 @@
+#!/bin/bash
+set -e
+
+# https://stackoverflow.com/a/1482133/270712
+MYDIR=dirname -- "$( readlink -f -- "$0"; )";
+pushd "$MYDIR"
+git pull
+docker compose up build
+popd