Merge pull request #102 from remicollet/issue-oldsphinx
authorMichael Wallner <mike@php.net>
Fri, 25 Dec 2020 10:58:44 +0000 (11:58 +0100)
committerGitHub <noreply@github.com>
Fri, 25 Dec 2020 10:58:44 +0000 (11:58 +0100)
fix doc build with old sphinx


Trivial merge