From: Stefano Zacchiroli Date: Mon, 12 Nov 2001 13:41:43 +0000 (+0000) Subject: Added ".db" suffix to urls_of_uris default value. X-Git-Tag: mlminidom_0_2_2~111 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=e274c41f35f93f700b48198ee2dc9a3eb38520c4;p=helm.git Added ".db" suffix to urls_of_uris default value. --- diff --git a/helm/configuration/configure.in b/helm/configuration/configure.in index 9a0f3fb7b..03c923e9d 100644 --- a/helm/configuration/configure.in +++ b/helm/configuration/configure.in @@ -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