X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fconfiguration%2Flib%2Fconfiguration.pl.in;h=6540b800ede6a287f8490921dda19bff70ca69bb;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=e88d8fbe715fb7b429bc1ebbd44c22591664e8ec;hpb=352196141500ca64f5a0d84218318ed78fdf830a;p=helm.git diff --git a/helm/configuration/lib/configuration.pl.in b/helm/configuration/lib/configuration.pl.in index e88d8fbe7..6540b800e 100644 --- a/helm/configuration/lib/configuration.pl.in +++ b/helm/configuration/lib/configuration.pl.in @@ -1,11 +1,36 @@ +# Copyright (C) 2000, HELM Team. +# +# This file is part of HELM, an Hypertextual, Electronic +# Library of Mathematics, developed at the Computer Science +# Department, University of Bologna, Italy. +# +# HELM is free software; you can redistribute it and/or +# modify it under the terms of the GNU General Public License +# as published by the Free Software Foundation; either version 2 +# of the License, or (at your option) any later version. +# +# HELM is distributed in the hope that it will be useful, +# but WITHOUT ANY WARRANTY; without even the implied warranty of +# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +# GNU General Public License for more details. +# +# You should have received a copy of the GNU General Public License +# along with HELM; if not, write to the Free Software +# Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA. +# +# For details, see the HELM World-Wide-Web page, +# http://cs.unibo.it/helm/. + use XML::Parser; use Env; -my $HELM_CONFIGURATION_PREFIX = $ENV{"HELM_CONFIGURATION_PREFIX"}; +my $HELM_CONFIGURATION_DIR = $ENV{"HELM_CONFIGURATION_DIR"}; +my $DEFAULT_HELM_CONFIGURATION_DIR = "@HELM_ETC_DIR@"; # this should be the only fixed constant -if (defined ($HELM_CONFIGURATION_PREFIX) { - $configuration_file = - $HELM_CONFIGURATION_PREFIX."/etc/helm/configuration.xml"; +if (defined ($HELM_CONFIGURATION_DIR)) { + $configuration_file = $HELM_CONFIGURATION_DIR."/configuration.xml"; +} else { + $configuration_file = $DEFAULT_HELM_CONFIGURATION_DIR."/configuration.xml"; } $parser = new XML::Parser(Handlers => {Start => \&handle_start,