]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 0c94f81) | patch
Patch by Paolo Tranquilli. It fixes the following problem: when a new
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 8 Apr 2013 12:20:15 +0000 (12:20 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 8 Apr 2013 12:20:15 +0000 (12:20 +0000)
commit8ca065f520dec7152df8e094028119515810b434
treee5bd6d9d1a0ce9b77063e09a2bdb1111cf7592dftree | snapshot
parent0c94f81f769d3c7377811a584f647553ebe7ceafcommit | diff
Patch by Paolo Tranquilli. It fixes the following problem: when a new
tab was openened, the interface got confused about which script was focused.
It did not save the previous focused script if it was at end of file and
it saved it instead when switching from the new tab. Other bugs could be related
to that.
matita/matita/matitaGui.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.