aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/cWarnings.mli
Commit message (Expand)AuthorAge
* [warnings] Remove `set_current_loc` hack.Gravatar Emilio Jesus Gallego Arias2018-04-11
* Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
* deprecate Pp.std_ppcmds type aliasGravatar Matej Košík2017-07-27
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* [location] Make location optional in Loc.locatedGravatar Emilio Jesus Gallego Arias2017-04-25
* Fix various shortcomings of the warnings infrastructure.Gravatar Maxime Dénès2016-11-02
* A new infrastructure for warnings.Gravatar Maxime Dénès2016-06-29