From 0af27540c1be9d6979bd1722cba7841daee945a7 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 17 Nov 2000 11:47:10 +0000
Subject: [PATCH] Nothing important

---
 helm/configuration/local/etc/helm/configuration.xml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/helm/configuration/local/etc/helm/configuration.xml b/helm/configuration/local/etc/helm/configuration.xml
index 78236e39b..76e062427 100644
--- 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>
-- 
2.39.2