From c42e0cb261536e634f4c2390a0146f6c4f8b1488 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ulysse=20G=C3=A9rard?= Date: Mon, 13 May 2024 19:31:34 +0200 Subject: [PATCH] Restore merging of cmi and cmt paths This was accidentally removed in c2d0346eab49d761b3cac240cfe3facb6134d0e9 --- src/kernel/mconfig.ml | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/kernel/mconfig.ml b/src/kernel/mconfig.ml index 0ec794d37..b17258bd5 100644 --- a/src/kernel/mconfig.ml +++ b/src/kernel/mconfig.ml @@ -242,6 +242,8 @@ let merge_merlin_config dot merlin ~failures ~config_path = source_path = dot.source_path @ merlin.source_path; hidden_build_path = dot.hidden_build_path @ merlin.hidden_build_path; hidden_source_path = dot.hidden_source_path @ merlin.hidden_source_path; + cmi_path = dot.cmi_path @ merlin.cmi_path; + cmt_path = dot.cmt_path @ merlin.cmt_path; exclude_query_dir = dot.exclude_query_dir || merlin.exclude_query_dir; use_ppx_cache = dot.use_ppx_cache || merlin.use_ppx_cache; extensions = dot.extensions @ merlin.extensions;