plugin-ext-metrics extension for creating metrics from language plugins#6303

Merged

tsmaeder merged 1 commit intoeclipse-theia:masterfrom JPinkney:plugin-ext-metrics

Nov 18, 2019

+1,434

Commits on Nov 7, 2019

Created plugin-ext-metrics for creating metrics from language plugins

JPinkney
authored and
che
committed