Fix the long name of the Common Public License
[debian-policy.git] / README-css.el
blob7dfb41b2ca01b895c2a8f7720f95ac6a055e745e
1 (setq
2 org-export-html-style-include-default nil
3 org-export-html-style
5 <style type=\"text/css\">
6 html { font-family: Times, serif; font-size: 12pt; }
7 .title { text-align: center; }
8 p.verse { margin-left: 3% }
9 pre {
10 border: 1pt solid #AEBDCC;
11 color: #000000;
12 background-color: LightSlateGray;
13 padding: 5pt;
14 font-family: \"Courier New\", courier, monospace;
15 font-size: 90%;
16 overflow:auto;
18 dt { font-weight: bold; }
19 div.figure { padding: 0.5em; }
20 div.figure p { text-align: center; }
21 .linenr { font-size:smaller }
22 .code-highlighted {background-color:#ffff00;}
23 .org-info-js_info-navigation { border-style:none; }
24 #org-info-js_console-label { font-size:10px; font-weight:bold;
25 white-space:nowrap; }
26 .org-info-js_search-highlight {background-color:#ffff00; color:#000000;
27 font-weight:bold; }
29 body {
30 color: black;
31 background-color: white;
32 font-family: Palatino, \"Palatino Linotype\", \"Hoefler Text\", \"Times New Roman\", Times, Georgia, Utopia, serif;
34 .org-agenda-date { color: #87cefa; }
35 .org-agenda-structure { color: #87cefa; }
36 .org-scheduled { color: #98fb98; }
37 .org-scheduled-previously { color: #ff7f24; }
38 .org-scheduled-today { color: #98fb98; }
39 .org-tag { font-weight: bold; }
40 .org-todo {
41 color: #ffc0cb;
42 font-weight: bold;
45 a:hover { text-decoration: underline; }
46 .todo { font-weight:bold; }
47 .done { font-weight:bold; }
48 .TODO { color:red; }
49 .WAITING { color:orange; }
50 .DONE { color:green; }
51 .timestamp { color: grey }
52 .timestamp-kwd { color: CadetBlue }
53 .tag { background-color:lightblue; font-weight:normal }
54 .target { background-color: lavender; }
55 table {
56 border-collapse: collapse; /*separate; */
57 border: outset 3pt;
58 border-spacing: 0pt;
59 /* border-spacing: 5pt; */
61 table td { vertical-align: top; border: 1px solid; }
62 table th { vertical-align: top; border: 2px solid; }
63 </style>
64 <script =\"text/javascript\" language=\"JavaScript\" src=\"/styles/org-info.js\"></script>
65 <script type=\"text/javascript\" language=\"JavaScript\">
66 /* <![CDATA[ */
67 org_html_manager.set(\"LOCAL_TOC\", 0);
68 org_html_manager.set(\"VIEW_BUTTONS\", 1);
69 org_html_manager.set(\"VIEW\", \"info\");
70 org_html_manager.set(\"TOC\", 1);
71 org_html_manager.set(\"MOUSE_HINT\", \"underline\"); // could be a background-color like #eeeeee
72 org_html_manager.setup ();
73 /* ]]> */
74 </script>