Restore merging of cmi and cmt paths

This was accidentally removed in c2d0346
voodoos · May 13, 2024 · c42e0cb · c42e0cb
1 parent 25bb400
commit c42e0cb
Showing 1 changed file with 2 additions and 0 deletions.
diff --git 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;