etc/options
changeset 48486 691d0b44a793
parent 48468 7f2998b95249
child 48492 03530cf284ca
     1.1 --- a/etc/options	Tue Jul 24 21:07:54 2012 +0200
     1.2 +++ b/etc/options	Tue Jul 24 21:26:28 2012 +0200
     1.3 @@ -22,3 +22,9 @@
     1.4  
     1.5  declare condition : string = ""
     1.6  
     1.7 +declare show_question_marks : bool = true
     1.8 +
     1.9 +declare names_long : bool = false
    1.10 +declare names_short : bool = false
    1.11 +declare names_unique : bool = true
    1.12 +