etc/options
changeset 67395 b39d596b77ce
parent 67273 c573cfb2c407
child 67506 30233285270a
     1.1 --- a/etc/options	Tue Jan 09 20:03:14 2018 +0100
     1.2 +++ b/etc/options	Tue Jan 09 20:15:36 2018 +0100
     1.3 @@ -214,8 +214,11 @@
     1.4  public option spell_checker_dictionary : string = "en"
     1.5    -- "spell-checker dictionary name"
     1.6  
     1.7 -public option spell_checker_elements : string = "words,comment,inner_comment,ML_comment,SML_comment"
     1.8 -  -- "relevant markup elements for spell-checker, separated by commas"
     1.9 +public option spell_checker_include : string = "words,comment,inner_comment,ML_comment,SML_comment"
    1.10 +  -- "included markup elements for spell-checker (separated by commas)"
    1.11 +
    1.12 +public option spell_checker_exclude : string = "antiquoted"
    1.13 +  -- "excluded markup elements for spell-checker (separated by commas)"
    1.14  
    1.15  
    1.16  section "Secure Shell"