]> matita.cs.unibo.it Git - helm.git/commitdiff
bug: HELM_VAR_DIR ==> HELM_LIBRARY_DIR
authorLuca Padovani <luca.padovani@unito.it>
Tue, 6 Feb 2001 11:02:04 +0000 (11:02 +0000)
committerLuca Padovani <luca.padovani@unito.it>
Tue, 6 Feb 2001 11:02:04 +0000 (11:02 +0000)
helm/configuration/etc/configuration.xml.in

index ad4e62aba036231a30bd57e13265342b44d05e90..b05eced388be4cea47acd4e8c28efe661d3fbf24 100644 (file)
@@ -26,7 +26,7 @@
 <!-- http://cs.unibo.it/helm/.                                         -->
 
 <configuration>
- <helm_dir>@HELM_VAR_DIR@</helm_dir>
+ <helm_dir>@HELM_LIBRARY_DIR@</helm_dir>
 
  <dtd_dir>@HELM_DTD_DIR@</dtd_dir>
  <servers_file>@HELM_SERVERS_FILE@</servers_file>