ankidroid/Anki-Android — pull request #161 by chajadan (2014-01-05 08:44:12+00:00)
Title: Implement default font as seperate from override font

First we had override font functionality named default font, then we matched its function to its name, people complained about a lost ability the want so we reinstated its override behavior back at square one. Pull request #160 (which is superceded by (i.e. fully incorporated into) this pull request) made the name match the behavior, and now this finishes it all off by having both functionalities present, and aptly named ;)

The design is as follows: default font will be set on any element that has no font otherwise specified for it, override font will override any font settings that have been specified, including default font. Override font is a simplistic way for a user to control the appearance of decks they did not author, without having to get into anki workings. Override functionality is now more deserving of its name, being applied to all html elements that may have had a font specified for them in cases where it wasn't being applied before. You want a hammer, you have a hammer.

I am closing pull request #160 since it is part of this commit. If for some reason this change is ultimately rejected, then I will repost #160.