]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 2f3ced3) | patch
Bug fixed: the _advance method must delete the parsed text iff it was parsed
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 25 Jul 2005 14:17:37 +0000 (14:17 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 25 Jul 2005 14:17:37 +0000 (14:17 +0000)
commit8f186be42e6cba96a6093eea0860f5a14ed80e71
tree679d462de0228d7fd77665fabc52c91f7410af08tree | snapshot
parent2f3ced3c4fd4bca1aaeb0c95f64e1b4ec7ea2f46commit | diff
Bug fixed: the _advance method must delete the parsed text iff it was parsed
from the script itself (calling the getFuture method).
helm/matita/matita.txt diff | blob | history
helm/matita/matitaScript.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.