aboutsummaryrefslogtreecommitdiff
path: root/dev/doc/xml-protocol.md
AgeCommit message (Expand)Author
2020-01-21[xml-protocol doc] Fix link to vscoqRamkumar Ramachandra
2020-01-19Removing text saying XML is future of PG, adding explicitly vscoq as a userHugo Herbelin
2019-10-29Merge PR #10942: Describe XML tags used for highlighting diff textThéo Zimmermann
2019-10-27Fix link to `coq-notes.md`Michael D. Adams
2019-10-24Describe XML tags used for highlighting diff textJim Fehrle
2019-07-15TyposJim Fehrle
2019-05-21Fixing typos - Part 1JPR
2018-07-08Modify URLs in xml-protocol.mdRin Arakaki
2018-07-08Modify URLs in xml-protocol.mdRin Arakaki
2017-12-26[ide] [doc] Document tweak to Query call.Emilio Jesus Gallego Arias
2017-10-06Make the XML protocol doc more version-independentThéo Zimmermann
2017-09-19Improve documentation of Status message.Maxime Dénès
2017-06-18[ide] Add route_id parameter to query call.Emilio Jesus Gallego Arias
2017-04-14Fix EOL characters in xml protocol documentation.Maxime Dénès
2017-04-13update XML protocol doc to 8.6Paul Steckler
2017-04-13add XML protocol doc for 8.5Paul Steckler