]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 04ca589) | patch
- added "clear alias" menu item
authorStefano Zacchiroli <zack@upsilon.cc>
Thu, 29 Jan 2004 13:25:52 +0000 (13:25 +0000)
committerStefano Zacchiroli <zack@upsilon.cc>
Thu, 29 Jan 2004 13:25:52 +0000 (13:25 +0000)
commit8498344c49c66aa84cf7484fdbd9c292f9aae5c6
treeaba050d80899f95a1838385f82e075b68c4ab059tree | snapshot
parent04ca589d65bcef6bd46cf4d277a748a12e09234bcommit | diff
- added "clear alias" menu item
- added "clear" button to the "edit aliases" window
helm/gTopLevel/gTopLevel.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.