Github user patricklucas commented on the issue:
https://github.com/apache/flink/pull/6396
The "hotfix" was a necessary modification to the dev-only helper scripts
for building the docs locally. I assumed that it would just get squashed into
the main commit when being merged, though I can do that too if it's required.
I don't think it's really deserving of its own issue/PR.---
