Add notes regarding CI usage
authorJean THOMAS <git0@pub.jeanthomas.me>
Wed, 22 Jul 2020 15:24:09 +0000 (17:24 +0200)
committerJean THOMAS <git0@pub.jeanthomas.me>
Wed, 22 Jul 2020 15:24:09 +0000 (17:24 +0200)
commit49d9c6fba7d4645a670062cb1a2c94988ec1317e
treeb37eff7e4c6684b7a6d5f532a2f2a00e9c597b72
parent63dd35e9309d5418e725525a2d3d51ddd3d48aa9
Add notes regarding CI usage
doc/development.md