etc/options
changeset 67506 30233285270a
parent 67395 b39d596b77ce
child 67743 7bd0a250183b
     1.1 --- a/etc/options	Thu Jan 25 14:13:55 2018 +0100
     1.2 +++ b/etc/options	Thu Jan 25 15:21:05 2018 +0100
     1.3 @@ -217,7 +217,7 @@
     1.4  public option spell_checker_include : string = "words,comment,inner_comment,ML_comment,SML_comment"
     1.5    -- "included markup elements for spell-checker (separated by commas)"
     1.6  
     1.7 -public option spell_checker_exclude : string = "antiquoted"
     1.8 +public option spell_checker_exclude : string = "no_words,antiquoted"
     1.9    -- "excluded markup elements for spell-checker (separated by commas)"
    1.10  
    1.11