diff -r e56c71c6b45e Doc/tools/sphinxext/indexsidebar.html --- a/Doc/tools/sphinxext/indexsidebar.html Sat Apr 05 15:35:01 2014 +0200 +++ b/Doc/tools/sphinxext/indexsidebar.html Mon Jun 02 15:39:12 2014 +0200 @@ -4,14 +4,15 @@