]> matita.cs.unibo.it Git - helm.git/commit
added style_dir in configuration file
authorLuca Padovani <luca.padovani@unito.it>
Thu, 8 Feb 2001 10:05:20 +0000 (10:05 +0000)
committerLuca Padovani <luca.padovani@unito.it>
Thu, 8 Feb 2001 10:05:20 +0000 (10:05 +0000)
commit303c659d6bd6d86314ebacfbf85360fdd6345e08
tree1f9da0635350b42c646f39e54b97780a684ac9ab
parent26f5337108946df050f07c68ebe9bc07b1fde173
added style_dir in configuration file
tmpdir is now tmp_dir
helm/configuration/etc/configuration.dtd
helm/configuration/etc/configuration.xml.in