From 05241aea30d01c8574c2c1c84dafa1bcc602ece5 Mon Sep 17 00:00:00 2001
From: Quentin Barrand <quba@redhat.com>
Date: Wed, 31 Aug 2022 11:05:29 +0200
Subject: [PATCH] Remove the `docs` GitHub Actions.

PlantUML relies on system fonts which are different from one machine to
the other. This is tricky to troubleshoot and blocks all PRs currently.
We will discuss in the community if we want to keep PlantUML or move to
something more popular such as Mermaid.
---
 .github/workflows/docs.yaml | 37 -------------------------------------
 1 file changed, 37 deletions(-)
 delete mode 100644 .github/workflows/docs.yaml

diff --git a/.github/workflows/docs.yaml b/.github/workflows/docs.yaml
deleted file mode 100644
index f2374ec9e..000000000
--- a/.github/workflows/docs.yaml
+++ /dev/null
@@ -1,37 +0,0 @@
-name: Docs
-
-on: [pull_request]
-
-jobs:
-  build-compare:
-    name: Build and compare docs
-    runs-on: ubuntu-latest
-
-    steps:
-      - uses: actions/checkout@v3
-
-      - uses: actions/setup-python@v4
-        with:
-          cache: pip
-          python-version: 3.x
-
-      - name: Install mkdocs
-        run: pip install -r docs/requirements.txt
-
-      - name: Install Java for PlantUML
-        run: |
-          sudo apt update
-          sudo apt install -y default-jre
-
-      - name: Build the docs site
-        run: make docs
-
-      - name: Check if the output directory changed
-        run: |
-          git add -N docs/site
-
-          if ! git diff --quiet docs/site/ ':!docs/site/index.html' ':!docs/site/sitemap.xml*'; then
-            echo 'Changes detected; please run make -C docs.'
-            git diff docs/site ':!docs/site/index.html' ':!docs/site/sitemap.xml*'
-            exit 1
-          fi