[GitHub] flink pull request #5213: [Minor][docs][metrics] Fix typo of metrics docs

2018-01-08 Thread asfgit
Github user asfgit closed the pull request at: https://github.com/apache/flink/pull/5213 ---

[GitHub] flink pull request #5213: [Minor][docs][metrics] Fix typo of metrics docs

2018-01-03 Thread greghogan
Github user greghogan commented on a diff in the pull request: https://github.com/apache/flink/pull/5213#discussion_r159523422 --- Diff: docs/monitoring/metrics.md --- @@ -905,7 +903,7 @@ Thus, in order to infer the metric identifier: Job-/TaskManager