diff options
| author | Hendrik Tews | 2021-01-25 10:44:32 +0100 |
|---|---|---|
| committer | hendriktews | 2021-01-31 21:42:52 +0100 |
| commit | dfb51f30c7af1afdf563f7fd8c4d23e653432dd1 (patch) | |
| tree | b6d423a81bd9340df4a9263c3675d295c9e5dc27 /doc/ProofGeneral.texi | |
| parent | 0440589e579fba52c0248477cde08b93f9e4cb76 (diff) | |
fix typos and unicode single quotations in doc strings
Backported those typos that were fixed only in the manual texi
sources and not in the doc strings, from which the text was
imported. Convert a few symbols quoted with curved unicode single
quotations to ascii, such that make magic recognizes them.
Diffstat (limited to 'doc/ProofGeneral.texi')
0 files changed, 0 insertions, 0 deletions