2 org-export-html-style-include-default nil
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% }
10 border: 1pt solid #AEBDCC;
12 background-color: LightSlateGray;
14 font-family: \"Courier New\", courier, monospace;
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;
26 .org-info-js_search-highlight {background-color:#ffff00; color:#000000;
31 background-color: gainsboro;
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; }
47 background-color: inherit;
49 text-decoration: inherit;
51 a:hover { text-decoration: underline; }
52 .todo { font-weight:bold; }
53 .done { font-weight:bold; }
55 .WAITING { color:orange; }
56 .DONE { color:green; }
57 .timestamp { color: grey }
58 .timestamp-kwd { color: CadetBlue }
59 .tag { background-color:lightblue; font-weight:normal }
60 .target { background-color: lavender; }
62 border-collapse: collapse; /*separate; */
65 /* border-spacing: 5pt; */
67 table td { vertical-align: top; border: 1px solid; }
68 table th { vertical-align: top; border: 2px solid; }
70 <script =\"text/javascript\" language=\"JavaScript\" src=\"/styles/org-info.js\"></script>
71 <script type=\"text/javascript\" language=\"JavaScript\">
73 org_html_manager.set(\"LOCAL_TOC\", 0);
74 org_html_manager.set(\"VIEW_BUTTONS\", 1);
75 org_html_manager.set(\"VIEW\", \"info\");
76 org_html_manager.set(\"TOC\", 1);
77 org_html_manager.set(\"MOUSE_HINT\", \"underline\"); // could be a background-color like #eeeeee
78 org_html_manager.setup ();