diff --git a/tools/devtool b/tools/devtool index 85e1145587f..f374ea94d2d 100755 --- a/tools/devtool +++ b/tools/devtool @@ -510,6 +510,7 @@ cmd_build() { # We don't need any special privileges for the build phase, so we run the # container as the current user/group. run_devctr \ + --privileged \ --user "$(id -u):$(id -g)" \ --workdir "$workdir" \ ${extra_args} \ @@ -517,6 +518,10 @@ cmd_build() { ./tools/release.sh --libc $libc --profile $profile ret=$? + # Running as root would have created some root-owned files under the build + # dir. Let's fix that. + cmd_fix_perms + if [ ! -z "$revision" ]; then popd git branch -D $branch_name