Nothing important

[helm.git] / helm / configuration / local / etc / helm / configuration.xml

diff --git a/helm/configuration/local/etc/helm/configuration.xml b/helm/configuration/local/etc/helm/configuration.xml
index 78236e39ba1ceffe3376397221de846bff4c86d0..76e062427fd48e68bb7d75000026ed037442dc77 100644 (file)
--- a/helm/configuration/local/etc/helm/configuration.xml
+++ b/helm/configuration/local/etc/helm/configuration.xml
@@ -4,7 +4,7 @@
 <configuration>
  <helm_dir>/home/pauillac/coq3/sacerdot/HELM/V6.2/examples</helm_dir>
 
- <dtd_dir><value-of var="helm_dir"/>/dtd</dtd_dir>
+ <dtd_dir>/home/pauillac/coq3/sacerdot/HELM/dtd</dtd_dir>
  <servers_file>/home/pauillac/coq3/sacerdot/HELM/V6.2/servers.txt</servers_file>
  <uris_dbm>/home/pauillac/coq3/sacerdot/HELM/V6.2/urls_of_uris</uris_dbm>
  <dest><value-of var="helm_dir"/></dest>