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

---
 helm/configuration/local/etc/helm/configuration.xml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/helm/configuration/local/etc/helm/configuration.xml b/helm/configuration/local/etc/helm/configuration.xml
index 89dbae771..78236e39b 100644
--- a/helm/configuration/local/etc/helm/configuration.xml
+++ b/helm/configuration/local/etc/helm/configuration.xml
@@ -2,11 +2,11 @@
 <!DOCTYPE configuration SYSTEM "configuration.dtd">
 
 <configuration>
- <helm_dir>/home/pauillac/coq3/sacerdot/HELM/interface/V6.2/examples</helm_dir>
+ <helm_dir>/home/pauillac/coq3/sacerdot/HELM/V6.2/examples</helm_dir>
 
  <dtd_dir><value-of var="helm_dir"/>/dtd</dtd_dir>
- <servers_file>/home/pauillac/coq3/sacerdot/HELM/interface/V6.2/servers.txt</servers_file>
- <uris_dbm>/home/pauillac/coq3/sacerdot/HELM/interface/V6.2/urls_of_uris</uris_dbm>
+ <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>
  <indexname>index.txt</indexname>
  <tmpdir>/tmp</tmpdir>
-- 
2.39.2