[Phpmyadmin-devel] going to 82% by default ?

Hi, after reading the arguments about this from Florian, Sebastian, Isaac and Juergen, I think it's better for the majority of our users (with the default browser font size of 16) to set our default font size to 82%. Why 82% ? I experimented and this gives a good compromise (the monospace fonts look better than in 80%, for example in the Rows stats). Comments? Marc