<!-- User name. It is used down in this configuration file. If left
unspecified, name of the user executing matita will be used (as per
getent) -->
<!-- User name. It is used down in this configuration file. If left
unspecified, name of the user executing matita will be used (as per
getent) -->