]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: e134b6f) | 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)
commit3ef63c09695a55d3da601a554441b8a69daf54a9
tree045ddd62d2532e648c09ab2a46df70ae04657963tree | snapshot
parente134b6f156268364d3027e73910c19e9c7e09838commit | 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!)
matita/matitaScript.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.