aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/richpp.ml
Commit message (Expand)AuthorAge
* [pp] Fix bug in richpp Format use.Gravatar Emilio Jesus Gallego Arias2017-03-21
* [pp] Remove special tag type and handler from Pp.Gravatar Emilio Jesus Gallego Arias2017-03-21
* [ide] Dynamic printing width.Gravatar Emilio Jesus Gallego Arias2017-03-21
* [ide] richpp clenaupGravatar Emilio Jesus Gallego Arias2017-03-21
* [pp] Make feedback the only logging mechanism.Gravatar Emilio Jesus Gallego Arias2017-03-21