From: Claudio Sacerdoti Coen Date: Fri, 10 Nov 2000 17:54:40 +0000 (+0000) Subject: Many bug fixed X-Git-Tag: nogzip~183 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=92ccab409fa4ec217b9334b9bc3f6677ad95db9b;p=helm.git Many bug fixed --- diff --git a/helm/configuration/install b/helm/configuration/install index 5b19af19d..de2507459 100755 --- a/helm/configuration/install +++ b/helm/configuration/install @@ -6,7 +6,7 @@ echo "* Files will be installed in \$root/local/lib/helm and *" echo "* in \$root/local/lib/etc/helm/ *" echo "********************************************************" echo -n "\$root=" -read ROOT "buondi" +read ROOT echo cp local/lib/helm/configuration.pl $ROOT/local/lib/helm/ cp local/lib/helm/configuration.pl $ROOT/local/lib/helm/ diff --git a/helm/configuration/local/lib/helm/configuration.pl b/helm/configuration/local/lib/helm/configuration.pl index deea890a8..f761e7129 100644 --- a/helm/configuration/local/lib/helm/configuration.pl +++ b/helm/configuration/local/lib/helm/configuration.pl @@ -1,7 +1,10 @@ use XML::Parser; +use Env; +my $HELM_CONFIGURATION_PREFIX = $ENV{"HELM_CONFIGURATION_PREFIX"}; # this should be the only fixed constant -$configuration_file = "/home/cadet/sacerdot/local/etc/helm/configuration.xml"; +$configuration_file = + $HELM_CONFIGURATION_PREFIX."/local/etc/helm/configuration.xml"; $parser = new XML::Parser(Handlers => {Start => \&handle_start, End => \&handle_end,