From 294d693749123fe1b6c153800d00725c672074be Mon Sep 17 00:00:00 2001 From: Jeremie Dimino Date: Thu, 12 Apr 2018 12:43:14 +0100 Subject: [PATCH] Do not load the user configuration file when INSIDE_DUNE is set --- CHANGES.md | 6 ++++++ bin/main.ml | 6 +++++- 2 files changed, 11 insertions(+), 1 deletion(-) diff --git a/CHANGES.md b/CHANGES.md index 6afac432..b1bfb897 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -1,3 +1,9 @@ +next +---- + +- Do not load the user configuration file when running inside dune + (#..., @diml) + 1.0+beta20 (10/04/2018) ----------------------- diff --git a/bin/main.ml b/bin/main.ml index bf9eabd1..3d4519d2 100644 --- a/bin/main.ml +++ b/bin/main.ml @@ -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