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