--- a/etc/options Tue Jul 24 21:48:41 2012 +0200 +++ b/etc/options Tue Jul 24 21:54:49 2012 +0200 @@ -28,3 +28,5 @@ declare names_short : bool = false declare names_unique : bool = true +declare timing : bool = false +