annotate armadillo-2.4.4/docs/style.css @ 0:8b6102e2a9b0

Armadillo Library
author maxzanoni76 <max.zanoni@eecs.qmul.ac.uk>
date Wed, 11 Apr 2012 09:27:06 +0100
parents
children
rev   line source
max@0 1 body
max@0 2 {
max@0 3 font-family: "Trebuchet MS", Trebuchet, "DejaVu Sans", "Luxi Sans", "Liberation Sans", Arial, Helvetica, sans-serif;
max@0 4 color: #000000;
max@0 5 background-color: #FFFFFF;
max@0 6 /* font-size: 10pt; */
max@0 7 /* line-height: 120%; */
max@0 8 height: 110%;
max@0 9 }
max@0 10
max@0 11 /* In the above, "height: 110%;" is a hack for stylistic purposes.
max@0 12 It typically makes the browser place a scroll bar on the left,
max@0 13 thereby reducing the overall width of the page. This is necessary,
max@0 14 as some pages do not have enough content (height wise) to make
max@0 15 the scrollbar appear, while other pages are long enough to have
max@0 16 the scrollbar. When content is centered for stylistic purposes,
max@0 17 the content on "short" pages will be in a different place than
max@0 18 the content on "long" pages. This can be visually annoying when
max@0 19 navigating from a "short" page to a "long" page, or vice versa.
max@0 20 Forcing the scrollbar to always appear removes this problem.
max@0 21 */
max@0 22
max@0 23 pre
max@0 24 {
max@0 25 font-family: "DejaVu Sans Mono", "Liberation Mono", "Andale Mono", "Bitstream Vera Sans Mono", "Luxi Mono", monospace;
max@0 26 font-size: smaller;
max@0 27 color: #666666;
max@0 28 }
max@0 29
max@0 30 a
max@0 31 {
max@0 32 text-decoration: none;
max@0 33 color: #57a706;
max@0 34 }
max@0 35
max@0 36 a:hover
max@0 37 {
max@0 38 text-decoration: underline;
max@0 39 color: #57a706;
max@0 40 }
max@0 41
max@0 42 a.menu
max@0 43 {
max@0 44 text-decoration: none;
max@0 45 color: #CCCCCC;
max@0 46 }
max@0 47
max@0 48 a.menu:hover
max@0 49 {
max@0 50 text-decoration: none;
max@0 51 color: #57a706;
max@0 52 }
max@0 53
max@0 54 a.hidden, a.hidden:hover, a.hidden:active, a.hidden:link, a.hidden:visited
max@0 55 {
max@0 56 text-decoration: none;
max@0 57 border-bottom: 0px
max@0 58 }
max@0 59
max@0 60 table
max@0 61 {
max@0 62 /* border: 1px solid #000; */
max@0 63 /* display: block; */
max@0 64 border-collapse: collapse;
max@0 65 }
max@0 66
max@0 67 td.line
max@0 68 {
max@0 69 border-left: 2px solid rgb(204, 204, 204);
max@0 70 }
max@0 71