Revision a60f7bbd9957776bbfdb29a11b47705606f60780

Committed on 21/06/2022 3:08 am by Luca Realdi <luca.realdi@opencontent.it> [GitHub Diff]

Add execution metrics