Fabian Homborg 86ab81dadf Remove searchtools.js ... With sphinx 4.5.0: 1. Some of our builtins actually give results (cd, end, set) 2. Some give broken results (and, if, or) 3. Only "for" even triggers the help page we hacked in So this is of dubious use, and removing it gets us out of the awkward situation of shipping it. Plus upstream sphinx has ditched jquery, so we would have to rewrite it anyway.		2022-05-19 17:38:41 +02:00
..
static	Remove searchtools.js	2022-05-19 17:38:41 +02:00
__init__.py	Reformat	2020-11-22 14:39:48 +01:00
globaltoc.html	docs: Fix TOC text and put them in a div	2021-01-27 22:02:35 +01:00
layout.html	docs: Add copy buttons to all the codeblocks	2021-08-15 20:09:49 +02:00
localtoc.html	docs: Fix TOC text and put them in a div	2021-01-27 22:02:35 +01:00
theme.conf	docs: Add a brief summary of the changes to the theme	2020-10-04 15:09:20 +02:00