From c975a3d4320a574f36fcbd64bc87de4cfcafe73c Mon Sep 17 00:00:00 2001
From: Luca Colagrande <luca.colagrande3@gmail.com>
Date: Thu, 3 Oct 2024 19:24:55 +0200
Subject: [PATCH] ci: Encode `build-docker`->`deploy-docs` dependency

---
 .github/workflows/ci.yml           | 24 +++++++++++++++++++++++-
 .github/workflows/publish-docs.yml | 28 ----------------------------
 2 files changed, 23 insertions(+), 29 deletions(-)
 delete mode 100644 .github/workflows/publish-docs.yml

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 05b4fefb2..8b15858f4 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -45,7 +45,7 @@ jobs:
   # Docs #
   ########
 
-  docs:
+  build-docs:
     name: Build documentation
     runs-on: ubuntu-22.04
     needs: build-docker
@@ -59,6 +59,28 @@ jobs:
       - name: Build docs
         run: make docs
 
+  deploy-docs:
+    name: Deploy documentation
+    runs-on: ubuntu-22.04
+    needs: build-docker
+    if: github.event_name == 'push' && github.ref == 'refs/heads/main'
+    container:
+      image: ghcr.io/pulp-platform/snitch_cluster:${{ github.ref_name }}
+    steps:
+      - uses: actions/checkout@v2
+      # For some reason, the checkout is done by a different user,
+      # than that deploying to Github (root, possibly due to Docker).
+      # So we need to set the repository as a safe directory.
+      - name: Git config safe.directory
+        run: |
+          git config --global --add safe.directory $GITHUB_WORKSPACE
+      - name: Generate documentation sources
+        run: |
+          make doc-srcs
+          make doxygen-docs
+      - name: Build and deploy documentation
+        run: mkdocs gh-deploy --force
+
   #####################
   # Python unit tests #
   #####################
diff --git a/.github/workflows/publish-docs.yml b/.github/workflows/publish-docs.yml
deleted file mode 100644
index 23a53bf4a..000000000
--- a/.github/workflows/publish-docs.yml
+++ /dev/null
@@ -1,28 +0,0 @@
-# Copyright 2020 ETH Zurich and University of Bologna.
-# Licensed under the Apache License, Version 2.0, see LICENSE for details.
-# SPDX-License-Identifier: Apache-2.0
-name: publish-docs
-on:
-  push:
-    branches: [main]
-  workflow_dispatch:
-jobs:
-  deploy:
-    name: Deploy documentation
-    runs-on: ubuntu-22.04
-    container:
-      image: ghcr.io/pulp-platform/snitch_cluster:main
-    steps:
-      - uses: actions/checkout@v2
-      # For some reason, the checkout is done by a different user,
-      # than that deploying to Github (root, possibly due to Docker).
-      # So we need to set the repository as a safe directory.
-      - name: Git config safe.directory
-        run: |
-          git config --global --add safe.directory $GITHUB_WORKSPACE
-      - name: Generate documentation sources
-        run: |
-          make doc-srcs
-          make doxygen-docs
-      - name: Build and deploy documentation
-        run: mkdocs gh-deploy --force