]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: e1efca3) | patch
Bug fixed: goto_top used to reset the status to the first one and then
authorAndrea Asperti <andrea.asperti@unibo.it>
Thu, 4 Feb 2010 10:32:30 +0000 (10:32 +0000)
committerAndrea Asperti <andrea.asperti@unibo.it>
Thu, 4 Feb 2010 10:32:30 +0000 (10:32 +0000)
commitda85c90e3e68296f687c553769ff24744dd67166
tree89f0b6be3fcd168f27d70c3c33aa0f4ac90f7a8btree | snapshot
parente1efca300fbaeb8c69a691a428a084d89a2c058fcommit | diff
Bug fixed: goto_top used to reset the status to the first one and then
reset_buffer (re-implemented yesterday) used to do the time travel
again. Fixed by getting rid of goto_top.

Note: the old implementation was slightly more efficient since the
initial notation of Matita was not re-loaded every time you go back to
top. In practice, this does not seem to matter.
helm/software/matita/matitaScript.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.