]> matita.cs.unibo.it Git - helm.git/commitdiff
Patch to the hard-coded constant in http_getter.pl
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 31 Oct 2000 16:43:47 +0000 (16:43 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 31 Oct 2000 16:43:47 +0000 (16:43 +0000)
helm/interface/http_getter/http_getter.pl

index 9ea1641b7c7b2036ca3b71216267f3fa1a448b23..650a16a3b2a0179156317247e64bfda13c477bee 100755 (executable)
@@ -4,7 +4,7 @@
 use Env;
 my $HELM_CONFIGURATION_PREFIX = $ENV{"HELM_CONFIGURATION_PREFIX"};
 my $HELM_CONFIGURATION_PATH =
- $HELM_CONFIGURATION_PREFIX."local/lib/helm/configuration.pl";
+ $HELM_CONFIGURATION_PREFIX."/local/lib/helm/configuration.pl";
 # next require defines: $helm_dir, $html_link
 require $HELM_CONFIGURATION_PATH;