etc/options
changeset 69968 1a400b14fd3a
parent 69854 cc0b3e177b49
child 70121 61e26527480e
     1.1 --- a/etc/options	Sun Mar 24 17:45:00 2019 +0100
     1.2 +++ b/etc/options	Sun Mar 24 17:53:46 2019 +0100
     1.3 @@ -242,7 +242,7 @@
     1.4  public option spell_checker_include : string = "words,comment,comment1,comment2,comment3,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 = "no_words,antiquoted"
     1.8 +public option spell_checker_exclude : string = "antiquoted,raw_text"
     1.9    -- "excluded markup elements for spell-checker (separated by commas)"
    1.10  
    1.11