/* reference.css, a stylesheet for reference documentation */
div.legalnotice { font-size: 80%; }