diff -r a5970360c00b -r b90bcdaaba0e build_in_docker.sh
--- a/build_in_docker.sh	Fri May 20 18:41:18 2022 +0200
+++ b/build_in_docker.sh	Fri May 20 18:50:40 2022 +0200
@@ -4,6 +4,6 @@
 
 docker start $CONTAINER 
 echo exec docker with $*
-docker exec $CONTAINER bash -c build $*
+docker exec $CONTAINER bash -c "build $*"
 docker stop $CONTAINER