From bc6b9c9a107c72a0a08b6ff8c33392864399dd48 Mon Sep 17 00:00:00 2001 From: Theo Cabrerizo Diem Date: Mon, 27 May 2024 01:31:22 +0200 Subject: [PATCH] Update build_dist --- src/build_dist | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/build_dist b/src/build_dist index c8ecdcc15..b5e18d426 100755 --- a/src/build_dist +++ b/src/build_dist @@ -6,7 +6,9 @@ CUSTOM_PI_OS_PATH=$(<"${DIR}"/custompios_path) export CUSTOM_PI_OS_PATH export PATH=$PATH:$CUSTOM_PI_OS_PATH -test -d /tmp || ( mkdir /tmp && mount -t tmpfs devtmp /tmp) +test -d /tmp || mkdir /tmp +mount -t tmpfs devtmp /tmp +df -h "${CUSTOM_PI_OS_PATH}"/build_custom_os "$@"