diff --git a/aux/docker_devel.sh b/aux/docker_devel.sh new file mode 100755 index 0000000..3f710c5 --- /dev/null +++ b/aux/docker_devel.sh @@ -0,0 +1,3 @@ +#!/bin/sh + +docker build --progress=plain --build-arg bt="$1" --output . .