Bug Report

In metric definitions with long comments, the script metricsgen could take the metric description from a one-line comment starting with //metrics:. Some of these comments are wrongly prefixed with // metrics:, with an extra space, thus they are ignored by the script. For example, in internal/consensus/metrics.go and internal/state/metrics.go.

Moreover, the go formatter will automatically insert a space after //, breaking the metric descriptions.

Proposed solutions

Either:

• fix the formatter to not insert spaces in //metrics:, or
• add the affected lines lint commands to ignore the formatter, or
• change metricsgen to accept lines with // metrics:.