config¶
This file is used to set Dune’s global configuration, which is applicable across projects and workspaces.
The configuration file is normally ~/.config/dune/config on Unix systems
and %LOCALAPPDATA%/dune/config on Windows. However, for most Dune commands,
it is possible to specify an alternative configuration file with the
--config-file option. Command-line flags take precedence over the contents
of the config file. If --no-config or -p is passed, Dune will not
read this file.
The config file can contain the following stanzas: