chore: Add NOCACHE option to misc/build-in-docker

diff --git a/misc/build-in-docker b/misc/build-in-docker
index a6227bc894831562f56acb620c22113d5e0703c0..f6811c76d93b062fd43c008328aa2b6838be7fcb 100755 (executable)
--- a/misc/build-in-docker
+++ b/misc/build-in-docker
@@ -25,9 +25,10 @@ top_dir="$(dirname "$(realpath "$0")")/.."
 tag="ccache-build:$name"
 command="${COMMAND:-/source/ci/build}"
 interactive="${INTERACTIVE:+--interactive --tty}"
+nocache="${NOCACHE:+--no-cache}"
 
 # Build (if not exists):
-docker build -t "$tag" "${top_dir}/dockerfiles/$name"
+docker build -t "$tag" ${nocache} "${top_dir}/dockerfiles/$name"
 
 # Cache compilation across docker sessions
 mkdir -p "${top_dir}/build-in-docker"