diff --git a/conf/format-options.py b/conf/format-options.py index e0fa18055..176a3837c 100755 --- a/conf/format-options.py +++ b/conf/format-options.py @@ -241,6 +241,7 @@ class GroffTagReplacer(TagReplacer): if not punct: punct = '' text = re.sub(r'[\r\n\t]', ' ', m.group('text')) + text = re.sub(r'"', '""', text) return '{0}.R{1} "{2}" "{3}" "{4}"\n'.format(nl, format, brack, text, punct) return replacer @@ -305,7 +306,8 @@ class ManFormatter: def __groffize(self, text): """Encode text as groff text""" text = self.__tags.replace(text) - text = re.sub(r'(?