add helper script to build and push the different images

.docker/build_and_push_images.sh

@@ -0,0 +1,27 @@
+#!/usr/bin/env bash
+
+REGISTRY=registry.tudelft.nl
+REPOSITORY=scancontrol
+USER=samxl
+
+ROS_VERSION=humble
+
+set -e
+
+function build_image () {
+    if ! [[ $1 =~ ^(core|base|dev)$ ]]; then echo "wrong input, expected 'core', 'base', or 'dev'"; exit 0 ; fi
+    docker build . --target ${REPOSITORY}-$1 -t ${REGISTRY}/${USER}/${REPOSITORY}:${ROS_VERSION}-$1
+}
+
+function push_image () {
+    if ! [[ $1 =~ ^(core|base|dev)$ ]]; then echo "wrong input, expected 'core', 'base', or 'dev'"; exit 0 ; fi
+    docker push ${REGISTRY}/${USER}/${REPOSITORY}:${ROS_VERSION}-$1
+}
+
+build_image "core"
+build_image "base"
+build_image "dev"
+
+push_image "core"
+push_image "base"
+push_image "dev"