mkdocs: enforce sufficiently new version, and use mkdocs-exclude.

We want to use the mkdocs-exclude plugin, which lets us exclude
particular files from the output directory.  But plugins aren't
available in the debian-stable version of mkdocs, so ensure that we're
running a sufficiently new version.  If we aren't, gracefully just skip
building the documentation.

docs/mkdocs.do

@@ -1,9 +1,22 @@
 redo-ifchange doc.list
 xargs redo-ifchange ../mkdocs.yml <doc.list
 
-if type mkdocs >/dev/null 2>/dev/null; then
+# Most people don't have mkdocs installed, or are using an obsolete one,
-	(cd .. && mkdocs build)
+# so let's handle those cases gracefully.
-else
+ver=$(mkdocs --version 2>/dev/null | cut -d' ' -f3)
+check='
+import sys
+ok = sys.argv[1].split(".") >= ["1", "0", "4"]
+exit(not ok)
+'
+
+if ! type mkdocs >/dev/null 2>/dev/null; then
 	echo "Warning: mkdocs is missing; can't generate website." >&2
 	redo-ifcreate /usr/bin/mkdocs
+elif ! python -c "$check" "$ver"; then
+	echo "Warning: mkdocs is too old ($ver); need at least 1.0.4." >&2
+	mkd=$(which mkdocs 2>/dev/null || :)
+	[ -x "$mkd" ] && redo-ifchange "$mkd"
+else
+	(cd .. && mkdocs build --strict --clean)
 fi

docs/requirements.txt

@@ -0,0 +1,2 @@
+mkdocs>=1.0.4
+mkdocs-exclude

mkdocs.yml

@@ -9,8 +9,20 @@ extra_javascript:
   - fetchcode.js
 extra_css:
   - extra_style.css
+plugins:
+  - exclude:
+      glob:
+        - "t/*"
+        - "*.tmp"
+        - "*.gz"
+        - "*.tar"
+        - "*.pdf"
+        - "*.ps"
+        - "*.1"
+      regex:
+        - ".*~"
 
-pages:
+nav:
   - Introduction: index.md
   - Getting Started: GettingStarted.md
   - Contributing.md