[MediaWiki-commits] [Gerrit] operations/puppet[production]: role: set external url for prometheus beta/tools

Filippo Giunchedi has submitted this change and it was merged. ( https://gerrit.wikimedia.org/r/354975 ) Change subject: role: set external url for prometheus beta/tools .. role: set external url for prometheus beta/tools

[MediaWiki-commits] [Gerrit] operations/puppet[production]: role: set external url for prometheus beta

Filippo Giunchedi has uploaded a new change for review. ( https://gerrit.wikimedia.org/r/354975 ) Change subject: role: set external url for prometheus beta .. role: set external url for prometheus beta Change-Id: