etc/options
changeset 48661 9149ebdd0241
parent 48634 30a6e841390a
child 48795 bece259ee055
     1.1 --- a/etc/options	Fri Aug 03 13:55:51 2012 +0200
     1.2 +++ b/etc/options	Fri Aug 03 14:52:45 2012 +0200
     1.3 @@ -63,3 +63,6 @@
     1.4  declare timing : bool = false
     1.5    -- "global timing of toplevel command execution and theory processing"
     1.6  
     1.7 +declare timeout : real = 0
     1.8 +  -- "timeout for session build job (seconds > 0)"
     1.9 +