maxwidth: int;
maxdepth: int;
timeout: float;
+ use_library: bool;
use_paramod: bool;
use_only_paramod : bool;
+ close_more : bool;
dont_cache_failures: bool;
}
{maxwidth=3;
maxdepth=3;
timeout=Unix.gettimeofday() +.3.0;
+ use_library=false;
use_paramod=true;
use_only_paramod=false;
+ close_more=false;
dont_cache_failures=false}
;;