etc/options
changeset 48661 9149ebdd0241
parent 48634 30a6e841390a
child 48795 bece259ee055
equal deleted inserted replaced
48660:730ca503e955 48661:9149ebdd0241
    61   -- "print original source text rather than internal representation"
    61   -- "print original source text rather than internal representation"
    62 
    62 
    63 declare timing : bool = false
    63 declare timing : bool = false
    64   -- "global timing of toplevel command execution and theory processing"
    64   -- "global timing of toplevel command execution and theory processing"
    65 
    65 
       
    66 declare timeout : real = 0
       
    67   -- "timeout for session build job (seconds > 0)"
       
    68