From 64cbcc1b00fd52b79e46e330afa17a8591e10a94 Mon Sep 17 00:00:00 2001
From: Gabriele Bozzola <sbozzolator@gmail.com>
Date: Fri, 13 Sep 2024 14:42:32 -0700
Subject: [PATCH] Run documentation on main

Previously, the "docs" action was run only on pull requests. This means
that documentation is not generated and deployed when the commit reaches
main, leading to stale github pages. This commit ensures that
documentation is also run on main.
---
 .github/workflows/docs.yml | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/.github/workflows/docs.yml b/.github/workflows/docs.yml
index 487bb78878..260ee022a1 100644
--- a/.github/workflows/docs.yml
+++ b/.github/workflows/docs.yml
@@ -2,6 +2,10 @@ name: Documentation
 
 on:
   pull_request:
+  push:
+    branches:
+      - main
+    tags: '*'
 
 jobs:
   docbuild: