]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 8402a4a) | patch
methods eos, goto, advance and retract now catch Invalid_argument "Array.make"
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Wed, 31 Jan 2007 19:54:01 +0000 (19:54 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Wed, 31 Jan 2007 19:54:01 +0000 (19:54 +0000)
commit72da1278d1f4ae051aa1445a23db9f82e6ddf34d
tree8ba22606093c77821fe5bb581574b66a61fccd0atree | snapshot
parent8402a4a856b031916b1e2b1354b863933763fa58commit | diff
methods eos, goto, advance and retract now catch Invalid_argument "Array.make"
that is raised when the script is too big to be handled (this makes quit work!)
helm/software/matita/matitaScript.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.