Do not load the user configuration file when INSIDE_DUNE is set

This commit is contained in:
Jeremie Dimino 2018-04-12 12:43:14 +01:00
parent 7a3917b9e3
commit 294d693749
2 changed files with 11 additions and 1 deletions

View File

@ -1,3 +1,9 @@
next
----
- Do not load the user configuration file when running inside dune
(#..., @diml)
1.0+beta20 (10/04/2018)
-----------------------

View File

@ -235,7 +235,11 @@ let common =
match config_file with
| No_config -> Config.default
| This fname -> Config.load_config_file ~fname
| Default -> Config.load_user_config_file ()
| Default ->
if Config.inside_dune then
Config.default
else
Config.load_user_config_file ()
in
let config =
Config.merge config