aboutsummaryrefslogtreecommitdiff
path: root/ide/richpp.ml
AgeCommit message (Expand)Author
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