Merge pull request #700 from diml/ignore-config-file-inside-dune
Do not load the user configuration file when INSIDE_DUNE is set
This commit is contained in:
commit
0e7c127e7a
|
@ -1,3 +1,9 @@
|
||||||
|
next
|
||||||
|
----
|
||||||
|
|
||||||
|
- Do not load the user configuration file when running inside dune
|
||||||
|
(#..., @diml)
|
||||||
|
|
||||||
1.0+beta20 (10/04/2018)
|
1.0+beta20 (10/04/2018)
|
||||||
-----------------------
|
-----------------------
|
||||||
|
|
||||||
|
|
|
@ -235,7 +235,11 @@ let common =
|
||||||
match config_file with
|
match config_file with
|
||||||
| No_config -> Config.default
|
| No_config -> Config.default
|
||||||
| This fname -> Config.load_config_file ~fname
|
| 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
|
in
|
||||||
let config =
|
let config =
|
||||||
Config.merge config
|
Config.merge config
|
||||||
|
|
Loading…
Reference in New Issue