Skip to content

Commit

Permalink
Do not store warnings as cache bound objects during display requests
Browse files Browse the repository at this point in the history
  • Loading branch information
kLabz committed Jun 7, 2024
1 parent c850b65 commit 756db7d
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion src/context/common.ml
Original file line number Diff line number Diff line change
Expand Up @@ -436,7 +436,7 @@ let ignore_error com =
b

let module_warning com m w options msg p =
DynArray.add m.m_extra.m_cache_bound_objects (Warning(w,msg,p));
if com.display.dms_full_typing then DynArray.add m.m_extra.m_cache_bound_objects (Warning(w,msg,p));
com.warning w options msg p

(* Defines *)
Expand Down

0 comments on commit 756db7d

Please sign in to comment.