]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 8498344) | patch
- s/TexTermEditor/TermEditor/ (* former no longer appropriate)
authorStefano Zacchiroli <zack@upsilon.cc>
Thu, 29 Jan 2004 14:53:16 +0000 (14:53 +0000)
committerStefano Zacchiroli <zack@upsilon.cc>
Thu, 29 Jan 2004 14:53:16 +0000 (14:53 +0000)
commit8dc254e60fb7ee127568bf1b0e5050f49b5167e1
tree1f65430de29020019816e6a28d765ac14797d9a3tree | snapshot
parent8498344c49c66aa84cf7484fdbd9c292f9aae5c6commit | diff
- s/TexTermEditor/TermEditor/ (* former no longer appropriate)
- added "auto disambiguation" setting support
helm/gTopLevel/gTopLevel.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.