GPS: new gnatmetric.py plugin
The gnatmetrics plugin has been rewritten. This new version allows to compute metrics for a project and its subprojects, and it is possible to choose the options to pass to gnatmetric before launching it.