table.source { line-height:115%; font-size:9pt;}
td.code { font-size:10pt; background-color: #dfdfdf; }
div.src-line { border-left: 2px solid #174D8D; padding-left:10px; white-space:no-break; }
div#content { width: 600px; }
div#license { border-left:2px solid #ccc; padding-left:10px; margin-top:20px; }
div.version { background-color: #f0f0f0; padding:5px 20px; margin-bottom:80px; } 

ol {  list-style:none; }