Fix compile warnings: Doc string single quote #863
Merged
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Hello again!
When compiling proof general there are over 400 warnings! Some of these warnings might be important but it is hard to tell with this much noise. I would like to help reduce this noise.
Newer emacs emit warnings when that are unescaped single quotes in docstrings. I've spent a good chunk of time resolving this issue.
For symbols that link to a variable or function they should be written as: `symbol'
For symbols that should not link to anything as they are just a symbol they should be written as: \+`symbol'.
By going through and making sure symbols are quoted using this style, I was also able to simplify the documentation generator slightly which removes some false positives and removes a lot of "@samp{@code{symbol}}" and replaces it with "@code{symbol}" which seems better.