Move documentation-tools/ to documentation-generator/

.github/workflows/generate-documentation.yml

@@ -2,7 +2,7 @@ name: Generate documentation
 on:
   push:
     paths:
-    - 'documentation-tools/**'
+    - 'documentation-generator/**'
     - DOCUMENTATION.md
 
 jobs:
@@ -13,5 +13,4 @@ jobs:
         with:
           ref: gh-pages
       - name: Run generator
-        run: documentation-tools/generate.py
+        run: documentation-generator/run.py
-

documentation-generator/filter.py

@@ -8,7 +8,7 @@ import json
 import re
 import sys
 
-from generate import SHIFT_HEADING
+from run import SHIFT_HEADING
 
 
 def text_content(content):