From 5fc7ddf76df72b7676fa1b07d8df5580775437fd 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: