From 8cb5fef740725ee51ffed5022faa097f21336bcd Mon Sep 17 00:00:00 2001
From: John MacFarlane <jgm@berkeley.edu>
Date: Sat, 23 Jul 2011 12:03:33 -0700
Subject: [PATCH] HTML template: make TOC more customizable.

Users can now insert a header before the table of contents,
or include other styling.
Thanks to Bruce D'Arcus for the suggestion.
---
 default.html | 10 +++++++++-
 1 file changed, 9 insertions(+), 1 deletion(-)

diff --git a/default.html b/default.html
index 0e8d97fa0..387e4eb7d 100644
--- a/default.html
+++ b/default.html
@@ -50,7 +50,7 @@
 $if(html5)$
 <header>
 $else$
-<div id="header">
+<div id="$idprefix$header">
 $endif$
 <h1 class="title">$title$</h1>
 $for(author)$
@@ -66,7 +66,15 @@ <h4 class="date">$date$</h4>
 $endif$
 $endif$
 $if(toc)$
+$if(html5)$
+<nav id="$idprefix$TOC">
+$toc$
+</nav>
+$else$
+<div id="$idprefix$TOC">
 $toc$
+</div>
+$endif$
 $endif$
 $body$
 $for(include-after)$