Make extension compatible with MediaWiki 1.35.