]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: f268a4b) | patch
After a goto the focus is now grabbed back by the insertion window.
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 20 Jul 2005 16:27:40 +0000 (16:27 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 20 Jul 2005 16:27:40 +0000 (16:27 +0000)
commit570fd2488f0ba8c16105dc30dd25dd00b558f0fe
tree7a0b8e8d9f032071207deb5610ab2b7ac5e25fd8tree | snapshot
parentf268a4b949ad0ac525f73dbd5116722c2ca6f552commit | diff
After a goto the focus is now grabbed back by the insertion window.
helm/matita/matitaGui.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.