diff -r 70990e795657 Doc/tools/sphinxext/indexsidebar.html --- a/Doc/tools/sphinxext/indexsidebar.html Fri Apr 04 20:59:44 2014 +0200 +++ b/Doc/tools/sphinxext/indexsidebar.html Mon Jun 02 15:29:29 2014 +0200 @@ -4,14 +4,15 @@