diff options
Diffstat (limited to 'tools/template.html')
| -rw-r--r-- | tools/template.html | 21 |
1 files changed, 14 insertions, 7 deletions
diff --git a/tools/template.html b/tools/template.html index fd2e56b..ca63146 100644 --- a/tools/template.html +++ b/tools/template.html @@ -2,7 +2,7 @@ <html> <head> <meta charset="UTF-8"> -<title>${title}</title> +<title>$title$</title> <style type="text/css"> body { font-family: Helvetica, arial, freesans, clean, sans-serif; line-height: 1.4; @@ -19,6 +19,7 @@ h3 { font-size: 110%; font-weight: bold; } h4 { font-size: 100%; font-weight: bold; } a.definition { font-weight: bold; } span.space { position: relative; } +span.number:after { content: " " } span.space:after { content: "·"; position: absolute; @@ -59,7 +60,7 @@ div.example > div:nth-child(3) { clear:right; background-color: #C9CaCE; } color: white; } #watermark a { color: white; } -a.dingus { color: red; cursor: pointer; } +a.dingus { margin-left: 1em; color: red; cursor: pointer; } a.footnoteRef > sup:before { content: "["; } @@ -85,7 +86,7 @@ a.footnoteRef > sup { a.dingus { display: none; } } </style> -<script src="//code.jquery.com/jquery-1.11.0.min.js"></script> +<script src="https://code.jquery.com/jquery-2.2.0.min.js"></script> <script type="text/javascript"> $$(document).ready(function() { $$("div.example").each(function(e) { @@ -102,10 +103,10 @@ $$(document).ready(function() { </script> </head> <body> -<h1 class="title">${title}</h1> -<div class="version">Version ${version} (${date})</div> +<h1 class="title">$title$</h1> +<div class="version">Version $version$ ($date$)</div> <div class="authors"> - <span class="author">${author}</span> + <span class="author">$author$</span> </div> <div class="license"> <a rel="license" @@ -123,6 +124,12 @@ $$(document).ready(function() { Commons Attribution-ShareAlike 4.0 International License</a>.</span> </div> <div id="watermark"></div> -${body} + +<div id="TOC"> +$toc$ +</div> + +$body$ + </body> </html> |