toc toggle button

The TOC toggle button was very small and inconspicuous. This patch
replaces the old one with small arrows placed at the right border
of the TOC header.
Code cleanup in html.php: html_toc() and html_list_toc() are obsolete
and have been removed.

darcs-hash:20050531184155-7ef76-249f948b2a8b71d45aab2b8418db2be5eb638f6d.gz

1 files changed, 2 insertions, 2 deletions

diff --git a/script.js b/script.js
index f43e9abbf..d25246c9c 100644
--- a/script.js
+++ b/script.js
@@ -291,10 +291,10 @@ function suggestWikiname(){
  */
 function showTocToggle(show,hide) {
   if(document.getElementById) {
-    document.writeln('<span class=\'toctoggle\'><a href="javascript:toggleToc()" class="toc">' +
+    document.writeln('<div class=\'toctoggle\'><a href="javascript:toggleToc()" class="toc">' +
     '<span id="showlink" style="display:none;">' + show + '</span>' +
     '<span id="hidelink">' + hide + '</span>'
-    + '</a></span>');
+    + '</a></div>');
   }
 }