From 1f829cda7957b48cac8109a3721ded11f6cec8de Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 12 Oct 2006 13:34:32 +0000 Subject: [PATCH] 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 | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/helm/software/components/tactics/auto.ml b/helm/software/components/tactics/auto.ml index 4acacefc6..b904d52cb 100644 --- a/helm/software/components/tactics/auto.ml +++ b/helm/software/components/tactics/auto.ml @@ -26,7 +26,7 @@ open AutoTypes;; open AutoCache;; -let debug_print s = () (*prerr_endline s;;*) +let debug_print s = () (* prerr_endline s;; *) (* {{{ *********** local given_clause wrapper ***********) @@ -571,7 +571,7 @@ let flags_of_params params ?(for_applyS=false) () = if timeout = 0 then if for_applyS then Unix.gettimeofday () +. 30.0 else - 0.0 + infinity else Unix.gettimeofday() +. (float_of_int timeout); AutoTypes.use_paramod = use_paramod; -- 2.39.2