From cb19ed3fc600f44b32029da2a515732c903f77b0 Mon Sep 17 00:00:00 2001
From: David Llewellyn-Jones <dllewellyn-jones@turing.ac.uk>
Date: Fri, 24 May 2024 14:00:03 +0100
Subject: [PATCH] Add manual trigger to the GitHub workflows

Adds a manual trigger, which can be useful if there are multiple
branches each with different versions of the documentation available.
---
 .github/workflows/pdflatex.yml | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/.github/workflows/pdflatex.yml b/.github/workflows/pdflatex.yml
index 366bdee..f635c99 100644
--- a/.github/workflows/pdflatex.yml
+++ b/.github/workflows/pdflatex.yml
@@ -3,6 +3,8 @@ on:
   push:
     branches-ignore:
       - 'gh-action-result/pdf-files'
+  workflow_dispatch:
+
 jobs:
   build_latex:
     runs-on: ubuntu-latest