aboutsummaryrefslogtreecommitdiff
path: root/ide/richpp.ml
AgeCommit message (Expand)Author
2018-05-24[ide] Move common protocol library to its own folder/object.Emilio Jesus Gallego Arias
2018-02-27Update headers following #6543.Théo Zimmermann
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-03-21[pp] Fix bug in richpp Format use.Emilio Jesus Gallego Arias
2017-03-21[pp] Remove special tag type and handler from Pp.Emilio Jesus Gallego Arias
2017-03-21[ide] Dynamic printing width.Emilio Jesus Gallego Arias
2017-03-21[ide] richpp clenaupEmilio Jesus Gallego Arias
2017-03-21[pp] Make feedback the only logging mechanism.Emilio Jesus Gallego Arias