fix double punctuation mark in docs
Merge pull request #3413 from timoschilling/doc_punctuation_mark

fix double punctuation mark in docs