other minor tweaks - doc generation should still be broken
authorparmentelat <thierry.parmentelat@inria.fr>
Sun, 20 May 2018 12:40:59 +0000 (14:40 +0200)
committerparmentelat <thierry.parmentelat@inria.fr>
Sun, 20 May 2018 12:40:59 +0000 (14:40 +0200)

No differences found