]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 303c659) | patch
styles_dir is now style_dir
authorLuca Padovani <luca.padovani@unito.it>
Thu, 8 Feb 2001 10:35:15 +0000 (10:35 +0000)
committerLuca Padovani <luca.padovani@unito.it>
Thu, 8 Feb 2001 10:35:15 +0000 (10:35 +0000)
commit42fe83d4b539b28d933cb6c81895afd810c2f316
tree11b6c1738da9f3df29579736980acc6dac217e45tree | snapshot
parent303c659d6bd6d86314ebacfbf85360fdd6345e08commit | diff
styles_dir is now style_dir
the getter now recognize one further command, getstyleconf, to retrieve
the stylesheet configuration file (and possibly its dtd)
helm/http_getter/http_getter.pl.in diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.