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