Added by Christos Stathis almost 12 years ago
Smaller font size for statistics (issue #2372)
View differences