]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: ad02924) | patch
Bug fixed: clicking on a new position while advancing/retracting now
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 18 Jul 2005 16:48:43 +0000 (16:48 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 18 Jul 2005 16:48:43 +0000 (16:48 +0000)
commitc91c06bd374f5edbed5c562d7fb1858058307a7a
tree308fa55144328873ef957b161c9e7fc152231b70tree | snapshot
parentad0292419b0204384ff55c946a6aabb73a47c42bcommit | diff
Bug fixed: clicking on a new position while advancing/retracting now
does absolutely nothing (i.e. at the very end of the execution the cursor
is at the end of the blue area).
helm/matita/matitaScript.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.