environment variable for diff-command

[raphael-proust]

Desired Behavior

I'd like there to be a DUNE_DIFF_COMMAND environment variable. Currently, the --diff-command flag works, but it being a flag is impractical (I only need it for some commands, I don't want to include it in aliases and wrappers).

The --diff-command is somewhat similar to EDITOR or MANPAGER/PAGER in that it's for selecting an orthogonal binary to delegate a dedicated task to.

Alternatively, a global dune configuration a la .gitconfig could work. Something I can put in my $HOME with a line that says (diff-command <…>).

Example

$ export DUNE_DIFF_COMMAND=delta
$ dune build @fmt 
<output similar to current `dune build @fmt --diff-command=delta>

[rgrinberg]

Seems fine to add this. A PR would be welcome.