]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: ade4052) | patch
removed "tilde_expand" hack: for the moment it is not needed (we can use $HOME)
authorStefano Zacchiroli <zack@upsilon.cc>
Thu, 2 Feb 2006 16:22:23 +0000 (16:22 +0000)
committerStefano Zacchiroli <zack@upsilon.cc>
Thu, 2 Feb 2006 16:22:23 +0000 (16:22 +0000)
commitc4eec8df32b6b004e76cbce54342385d3bf25fa5
tree20fd05ba494647574b6027e8df25e9a0923e5adatree | snapshot
parentade4052a34236f21fb0d2e720ae70000373d90c1commit | diff
removed "tilde_expand" hack: for the moment it is not needed (we can use $HOME)
if it will be needed in the future it should be implemented (properly) in the
registry itself
helm/matita/matitaInit.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.