Utility for unescaping HTML entities leftover from MediaWiki->rST conversion

(imported from commit 2f2507f299c3d09c67bfd26d6c11fab47431d935)

docs/html_unescape.py

@@ -0,0 +1,9 @@
+#!/usr/bin/env python3
+
+# Remove HTML entity escaping left over from MediaWiki->rST conversion.
+
+import html
+import sys
+
+for line in sys.stdin:
+    print(html.unescape(line), end='')

tools/lint-all

@@ -31,6 +31,7 @@ node_modules
 """.split()
 
 exclude_files = """
+docs/html_unescape.py
 zproject/test_settings.py
 zproject/settings.py
 tools/jslint/jslint.js