From da5181799d1b6345d6c09742284d65a2b378d7cf Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jan=20Sch=C3=A4r?= Date: Fri, 4 Mar 2022 17:40:50 +0100 Subject: [PATCH] Clean up docker container after it stops --- tools/bfdocker.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tools/bfdocker.sh b/tools/bfdocker.sh index 4bb13e5..e0504c3 100755 --- a/tools/bfdocker.sh +++ b/tools/bfdocker.sh @@ -28,6 +28,6 @@ mkdir -p $BF_BUILD # run the command in the docker image with the same userid to avoid # permission problems later. -docker run -u $(id -u) -i -t \ +docker run -u $(id -u) --rm -i -t \ --mount type=bind,source=$BF_SOURCE,target=/source \ $BF_DOCKER