Github user fhueske commented on the issue:
https://github.com/apache/flink/pull/6161
Documentation fixes are usually not critical to include in a release
because the docs are always built from the most recent release branch. So also
documentation changes that are not included in a release will be published
shortly after being committed.
I'll merge this PR.
Btw. it is OK to create a hotfix (i.e., a PR without creating a JIRA issue)
for minor fixes like this.
Thanks, Fabian---
