]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 7278063) | 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)
commit1f829cda7957b48cac8109a3721ded11f6cec8de
tree9df9c9d8359a2d5dcc8f3aeab5821802978ce5fctree | snapshot
parent7278063faf0ebb5fd08af2191989a12e2a27f522commit | 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
helm/software/components/tactics/auto.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.