Quotation style

[Shark64]

Switch to logical quoting style, periods and comma at the ed of a quotation are put outside the quote.

[awodey]

BTW I believe this is standard British style.

Sent from my iPhone

On Dec 18, 2013, at 10:37 AM, Shark64 [email protected] wrote:

Switch to logical quoting style, periods and comma at the ed of a quotation are put outside the quote.

You can merge this Pull Request by running

git pull https://github.com/Shark64/book quote-style
Or view, comment on, or merge it at:

#588

Commit Summary

enable pdftex extensions with \usepackage{microtype}
Merge pull request #1 from HoTT/master
Merge pull request #2 from Shark64/microtype
Uniform logical quoting stile, command and period outside the quotation.
Revert "Merge pull request #2 from Shark64/microtype"
File Changes

M errata.tex (8)
M formal.tex (2)
M introduction.tex (10)
M logic.tex (6)
M preliminaries.tex (6)
Patch Links:

https://github.com/HoTT/book/pull/588.patch
https://github.com/HoTT/book/pull/588.diff

[mikeshulman]

It would be cleaner if this didn't have a merge-and-then-revert of #584, which seems like it may be a while before is it merged. Can it be rebased or cherrypicked or some other git magic to get rid of those commits?

[JasonGross]

One easy set of git commands to remove merge commits is (when you're on the appropriate branch, assuming upstream is HoTT/book and origin is Shark64/book):

git remote update
git rebase -i upstream master
# then close the editor that opens
git push origin quote-style:quote-style -f

See, e.g., http://code-redefined.blogspot.com/2010/11/git-rebase-tricks-cleaning-up-twisted.html for a longer explanation.

[JasonGross]

If you want to delete the merge-and-revert, you can do the above, but delete the lines that include commits that you don't want to keep.

An alternative is to do

git remote update
git checkout master
git pull upstream master:master --ff-only # or use --rebase or whatever if you have changes to master
git checkout -b quote-style-2
git cherry-pick 70e9bc1
git cherry-pick 70ea00b
git cherry-pick d976b6e
git push origin quote-style-2:quote-style -f
# now clean up branches
git checkout quote-style
git pull origin quote-style:quote-style -f
git branch -D quote-style-2

[andrejbauer]

I kindly ask that these pull requests be disentangled. The microtype thing requires careful consideration (leafing through some PDF files). I disagree with changes of .) to ).. As there is no way to partially pull a request, I am closing this one. Please open several new ones. The best way to do this is to create branches in your fork and then make pull requests from them.

[Shark64]

Ok, so the stile should be period outside the quotes but inside the parenthesis?
I'll try to cook some regexp and see how it works.

[mikeshulman]

Here is the rule I've always known for periods and parentheses: http://www.quickanddirtytips.com/education/grammar/periods-and-parentheses . I've never heard of differences across the Atlantic on this one; are there?

[awodey]

and here is the issue I was referring to, regarding periods and quotation marks:
http://www.quickanddirtytips.com/education/grammar/quotation-marks-with-periods-and-commas
the rules are different for US and UK.

On Jan 1, 2014, at 11:34 AM, Mike Shulman [email protected] wrote:

Here is the rule I've always known for periods and parentheses: http://www.quickanddirtytips.com/education/grammar/periods-and-parentheses . I've never heard of differences across the Atlantic on this one; are there?

—
Reply to this email directly or view it on GitHub.

[andrejbauer]

Irrespective of what the style should be, there should be three separate pull requests: periods and quotes, periods and parentheses, and microtype.