X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fhttp_getter%2Fhttp_getter.pl.in;h=addd81dccc1a2213455c10188072635257dd5985;hb=6d71aa3ee23468b86bcad8fb640d71e2692bd901;hp=cd474f17b2e088a0fe2d23e3f640bd2eded62df4;hpb=334e20b9e4e3976c2c95928f5b2b4a5fc5db81da;p=helm.git

diff --git a/helm/http_getter/http_getter.pl.in b/helm/http_getter/http_getter.pl.in
index cd474f17b..addd81dcc 100755
--- a/helm/http_getter/http_getter.pl.in
+++ b/helm/http_getter/http_getter.pl.in
@@ -34,7 +34,9 @@ if (defined ($HELM_LIB_DIR)) {
    $HELM_LIB_PATH = $DEFAULT_HELM_LIB_DIR."/configuration.pl";
 }
 
+# Let's override the configuration file
 $styles_dir = $ENV{"HELM_STYLE_DIR"} if (defined ($ENV{"HELM_STYLE_DIR"}));
+$dtd_dir = $ENV{"HELM_DTD_DIR"} if (defined ($ENV{"HELM_DTD_DIR"}));
 
 # <ZACK>: TODO temporary, move this setting to configuration file
 # set the cache mode, may be "gzipped" or "normal"