diff --git a/tools/devtool b/tools/devtool index 85e1145587f..f1a944aad03 100755 --- a/tools/devtool +++ b/tools/devtool @@ -510,13 +510,17 @@ 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 \ - --user "$(id -u):$(id -g)" \ + --privileged \ --workdir "$workdir" \ ${extra_args} \ -- \ ./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