]> matita.cs.unibo.it Git - helm.git/commitdiff
Added ".db" suffix to urls_of_uris default value.
authorStefano Zacchiroli <zack@upsilon.cc>
Mon, 12 Nov 2001 13:41:43 +0000 (13:41 +0000)
committerStefano Zacchiroli <zack@upsilon.cc>
Mon, 12 Nov 2001 13:41:43 +0000 (13:41 +0000)
helm/configuration/configure.in

index 9a0f3fb7bede4d1d9acb216a486b9d5def2a3255..03c923e9d4d89a9ec7f5231a288094db40e67cc2 100644 (file)
@@ -132,7 +132,7 @@ HELM_FONT_CONFIGURATION_PATH=$HELM_ETC_DIR/helm-font-configuration.xml
 dnl Only for HELM XML configuration
 HELM_LIBRARY_DIR=$HELM_VAR_DIR/library
 HELM_SERVERS_FILE=$HELM_VAR_DIR/servers.txt
-HELM_URIS_DBM=$HELM_VAR_DIR/urls_of_uris
+HELM_URIS_DBM=$HELM_VAR_DIR/urls_of_uris.db
 
 dnl CSC: FIXME: getters should download the DTDs
 HELM_DTD_DIR=$HELM_SHARE_DIR/dtd