tree 2b84d5a7fd057ac6bfd94625229b58dc1c15dd08
parent 52a803cb9d0021fc03b1a174915008994aa14adc
author Davide Pesavento <davidepesa@gmail.com> 1586407901 -0400
committer Davide Pesavento <davidepesa@gmail.com> 1586483286 -0400

ci+docs: minor cleanups

Change-Id: I280fd84d89061e34ad4e2aaa00ce63ad21b03565