Index: doc/_build/html/_static/doctools.js
===================================================================
diff -u -rd200c1a6509757b11288719d8aefb33a0d19512e -rf49c3222ca48631f1f40ff99230983710a7d1b34
--- doc/_build/html/_static/doctools.js	(.../doctools.js)	(revision d200c1a6509757b11288719d8aefb33a0d19512e)
+++ doc/_build/html/_static/doctools.js	(.../doctools.js)	(revision f49c3222ca48631f1f40ff99230983710a7d1b34)
@@ -4,7 +4,7 @@
  *
  * Sphinx JavaScript utilities for all documentation.
  *
- * :copyright: Copyright 2007-2013 by the Sphinx team, see AUTHORS.
+ * :copyright: Copyright 2007-2011 by the Sphinx team, see AUTHORS.
  * :license: BSD, see LICENSE for details.
  *
  */
@@ -32,7 +32,7 @@
  */
 jQuery.urldecode = function(x) {
   return decodeURIComponent(x).replace(/\+/g, ' ');
-};
+}
 
 /**
  * small helper function to urlencode strings
@@ -62,6 +62,18 @@
 };
 
 /**
+ * small function to check if an array contains
+ * a given item.
+ */
+jQuery.contains = function(arr, item) {
+  for (var i = 0; i < arr.length; i++) {
+    if (arr[i] == item)
+      return true;
+  }
+  return false;
+};
+
+/**
  * highlight a given string on a jquery object by wrapping it in
  * span elements with the given class name.
  */
@@ -168,9 +180,6 @@
     var terms = (params.highlight) ? params.highlight[0].split(/\s+/) : [];
     if (terms.length) {
       var body = $('div.body');
-      if (!body.length) {
-        body = $('body');
-      }
       window.setTimeout(function() {
         $.each(terms, function() {
           body.highlightText(this.toLowerCase(), 'highlighted');