dune install with root permission should not create files in the build directory #3857
Description
Expected Behavior
Calling sudo dune install then dune build or dune clean (without sudo) should not fail.
Actual Behavior
Calling dune install with sudo creates a build state which is not usable anymore for the regular user.
Reproduction
$ mkdir /tmp/test && cd /tmp/test
$ echo '(executable (public_name test))' > dune
$ touch test.ml test.opam
$ dune build @install
$ sudo $(which dune) install --prefix /tmp/test
$ dune clean
Error: unlink: _build/default/.dune/configurator.v2: Permission denied
$ dune build
Error: unlink: _build/default/.dune/configurator.v2: Permission denied
Specifications
- Version of
dune(output ofdune --version): 2.7.1