Rename OptimizationDiagnosticInfo.h to OptimizationRemarkEmitter.h
[polly-mirror.git] / www / menu.css
blobbb70a8f56f2f95b24b702a8bb62961d8399e7a1d
1 /***************/
2 /* page layout */
3 /***************/
5 #menu {
6 line-height: 1.3em;
7 width: 18em;
8 float: left;
9 margin-right: 3em;
10 padding: 1em;
11 background-color: #edf7ff;
13 /**************/
14 /* menu style */
15 /**************/
17 #menu .submenu {
18 display:block;
19 padding-top: 0.2em;
20 font-bottom: 1.2em;
24 * Color scheme
25 * blue: #556293
26 * red: #931e24
27 * brown: #937155
28 * green: #24931e
31 #menu label {
32 display:block;
33 color: white;
34 margin-bottom: 0.4em;
35 margin-top: 0.4em;
36 font-weight: bold;
37 font-size: 1.1em;
38 text-align: center;
39 background-color: #3b4567;
40 -webkit-border-radius: 5px;
41 -moz-border-radius: 5px;
42 border-radius: 5px;
43 padding-top: 0.2em;
44 padding-bottom: 0.2em;
47 #menu a {
48 padding:0 .2em;
49 -webkit-border-radius: 5px;
50 -moz-border-radius: 5px;
51 border-radius: 5px;
52 display:block;
53 font-weight: bold;
54 text-decoration: none;
55 color: #3b4567;
58 a.rss-item {
59 margin-bottom: -1.2em;
61 #menu a:visited {
64 #menu .submenu2 {
65 margin-top: 2em;
68 #menu .submenu2 label {
69 background-color: #f35555;
72 .rss-box {
73 padding: 0em;
76 li.rss-item {
77 padding-bottom: 0em;
80 .rss_item {
81 padding-top: 0em;
84 .rss-date {
85 font-size: 0.6em;
86 color: gray;
88 .rss-title {
89 font-size: 0.7em;
90 margin: 0px;