From 3b9b4329abde4eb175ab9d5c31c3fcb66f36d831 Mon Sep 17 00:00:00 2001
From: kuroz <shellpick@gmail.com>
Date: Tue, 22 May 2012 15:32:47 +0800
Subject: [PATCH] use document.body instead of getElementsByTagName

---
 generated_toc.js | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/generated_toc.js b/generated_toc.js
index e946a9d..8ca89ce 100644
--- a/generated_toc.js
+++ b/generated_toc.js
@@ -136,7 +136,7 @@ generated_toc = {
     // set top_node to be the element in the document under which
     // we'll be analysing headings
     if (generate_for == 'page') {
-      top_node = document.getElementsByTagName('body');
+      top_node = document.body;
     } else {
       // i.e., explicitly set to "parent", left blank (so "unset"),
       // or some invalid value