Removed outdated scripts for mkdocs + added check-docs ci

.github/workflows/docs.yml

@@ -0,0 +1,23 @@
+# Runs docs related jobs.
+# CI job heavily inspired by: https://github.com/tarides/changelog-check-action
+
+name: docs
+
+on:
+  pull_request:
+    types: [opened, reopened, synchronize, labeled, unlabeled]
+
+jobs:
+  documented:
+    runs-on: ubuntu-latest
+    steps:
+      - name: Checkout code
+        uses: actions/checkout@main
+        with:
+          fetch-depth: 0
+      - name: Check for changes in the docs directory
+        env:
+          BASE_REF: ${{ github.event.pull_request.base.ref }}
+          NO_DOCS_LABEL: ${{ contains(github.event.pull_request.labels.*.name, 'no docs') }}
+        run: ./scripts/check-docs.sh "${{ inputs.docs }}"
+        shell: bash

scripts/check-docs.sh

@@ -0,0 +1,21 @@
+#!/bin/bash
+set -uo pipefail
+
+DOCS_DIR="docs/"
+
+if [ "${NO_DOCS_LABEL}" = "true" ]; then
+    # 'no docs' label set, so finish successfully
+    echo "\"no docs\" label has been set"
+    exit 0
+else
+    # a docs check is required
+    # fail if the diff is empty (no changes in docs directory)
+    if git diff --quiet "origin/${BASE_REF}" -- "${DOCS_DIR}"; then
+        >&2 echo "Changes should be accompanied by documentation updates in the \"docs/\" directory.
+This behavior can be overridden by using the \"no docs\" label, which is used for changes
+that don't require documentation updates or are purely maintenance-related."
+        exit 1
+    fi
+
+    echo "The \"docs/\" directory has been updated."
+fi