my $documentroot = '/projects/matita/public_html/';
my $protohrc = $documentroot . 'helm-proto.hrc';
my $scriptsdir = $documentroot . 'library/';
my $documentroot = '/projects/matita/public_html/';
my $protohrc = $documentroot . 'helm-proto.hrc';
my $scriptsdir = $documentroot . 'library/';