tree 0f63a187b8e4450592f9ccfcfdccdaaed0aedb1a
parent db844a15c67693448706e3f220ac25959bcc711c
author David Ostrovsky <david@ostrovsky.org> 1595162378 +0200
committer David Ostrovsky <david@ostrovsky.org> 1595168818 +0200

Adapt to recent master

Change-Id: I2b6d6a9dfd1972943ab6f01678d82c58093fb83f