]> matita.cs.unibo.it Git - helm.git/commitdiff
configuration file changed
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 31 Oct 2000 16:06:43 +0000 (16:06 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 31 Oct 2000 16:06:43 +0000 (16:06 +0000)
helm/configuration/local/etc/helm/configuration.xml

index 0a007fc5bdec3a9dbf34706d2622f3345135ac33..1e4594bf1f7ee03543cfc967c5ed8143f5571419 100644 (file)
@@ -2,11 +2,11 @@
 <!DOCTYPE configuration SYSTEM "configuration.dtd">
 
 <configuration>
- <helm_dir>/home/pauillac/coq3/sacerdot/HELM/INTERFACE/examples</helm_dir>
+ <helm_dir>/home/pauillac/coq3/sacerdot/HELM/interface/examples</helm_dir>
 
  <dtd_dir><value-of var="helm_dir"/>/dtd</dtd_dir>
- <servers_file>/home/pauillac/coq3/sacerdot/HELM/INTERFACE/servers.txt</servers_file>
- <uris_dbm>/home/pauillac/coq3/sacerdot/HELM/INTERFACE/urls_of_uris</uris_dbm>
+ <servers_file>/home/pauillac/coq3/sacerdot/HELM/interface/servers.txt</servers_file>
+ <uris_dbm>/home/pauillac/coq3/sacerdot/HELM/interface/urls_of_uris</uris_dbm>
  <dest><value-of var="helm_dir"/></dest>
  <indexname>index.txt</indexname>
  <tmpdir>/tmp</tmpdir>