Dear dune devs,

doing man dune install shows many command line options which seem to have no effect, a example of such an option is --display.

I wonder whether this is due to the change that had dune install foo not calling dune build -p foo before.

Note that after having a quick look to dune install, indeed there could be a problem if dune install does indeed build things, as a typical workflow for distros is dune build -p foo && sudo dune install foo, so it is usually a desired invariant that no build happens in the install command as it is running with S.U. permissions.