]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 19451c8) | patch
timeout if unspecfied should be set to infinity, not 0, since the timeout inside...
authorEnrico Tassi <enrico.tassi@inria.fr>
Thu, 12 Oct 2006 13:34:32 +0000 (13:34 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Thu, 12 Oct 2006 13:34:32 +0000 (13:34 +0000)
commitece1b63a7eec3567ef9eda9bcd1550655a575d07
tree0edc28720fd50e46a3ca3c74876ab87149bdd888tree | snapshot
parent19451c84fa726b9a337b5e8647b4adbfb50db2dfcommit | diff
timeout if unspecfied should be set to infinity, not 0, since the timeout inside the flagfs structure is a time in the future, not a decreasing quantity.
every loop of auto the check gettimeofday() > timeout raise Fail
components/tactics/auto.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.