Browse Source

Do not store warnings as cache bound objects during display requests (#11687)

Rudy Ges 1 year ago
parent
commit
ec35baca4f
1 changed files with 1 additions and 1 deletions
  1. 1 1
      src/context/common.ml

+ 1 - 1
src/context/common.ml

@@ -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 *)