etc/options
changeset 48492 03530cf284ca
parent 48486 691d0b44a793
child 48513 ace120a2cb70
     1.1 --- a/etc/options	Tue Jul 24 21:48:41 2012 +0200
     1.2 +++ b/etc/options	Tue Jul 24 21:54:49 2012 +0200
     1.3 @@ -28,3 +28,5 @@
     1.4  declare names_short : bool = false
     1.5  declare names_unique : bool = true
     1.6  
     1.7 +declare timing : bool = false
     1.8 +