]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 0cb00e6) | patch
Ctr+Backspace is now enabled. Used to perform "alternative" deletion.
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 2 Jul 2003 10:30:01 +0000 (10:30 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 2 Jul 2003 10:30:01 +0000 (10:30 +0000)
commit65e3c9976212e04a4678ff9ce9e3c2f436d06d33
treed1781b54cdb2913c970a79fde089675cb3583f90tree | snapshot
parent0cb00e631ea54deacbfde12e1c458ca602b97870commit | diff
Ctr+Backspace is now enabled. Used to perform "alternative" deletion.
helm/gTopLevel/texTermEditor.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.