aboutsummaryrefslogtreecommitdiff
path: root/ide/xml_printer.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
2016-09-05xml_printer: use sensible names for putc and putsEnrico Tassi
2016-06-02Move ide serialization libraries from lib/ to ide/Emilio Jesus Gallego Arias