Move Doc/tools/sphinxext content to Doc/tools, there is no need for the nested subdirectory anymore.
diff --git a/Doc/Makefile b/Doc/Makefile
index fee7fc7..5b5f68a 100644
--- a/Doc/Makefile
+++ b/Doc/Makefile
@@ -8,7 +8,7 @@
SPHINXBUILD = sphinx-build
PAPER =
SOURCES =
-DISTVERSION = $(shell $(PYTHON) tools/sphinxext/patchlevel.py)
+DISTVERSION = $(shell $(PYTHON) tools/patchlevel.py)
ALLSPHINXOPTS = -b $(BUILDER) -d build/doctrees -D latex_paper_size=$(PAPER) \
$(SPHINXOPTS) . build/$(BUILDER) $(SOURCES)
@@ -79,7 +79,7 @@
@$(MAKE) build BUILDER=$(BUILDER) || { \
echo "Suspicious check complete; look for any errors in the above output" \
"or in build/$(BUILDER)/suspicious.csv. If all issues are false" \
- "positives, append that file to tools/sphinxext/susp-ignored.csv."; \
+ "positives, append that file to tools/susp-ignored.csv."; \
false; }
coverage: BUILDER = coverage