From 0d0540c4eb58447130f4c80e1d104f85028f06fa Mon Sep 17 00:00:00 2001
From: David Holland <dholland@galois.com>
Date: Fri, 31 Jan 2025 17:22:12 -0500
Subject: [PATCH] CI: add more comments, pursuant to previous changes

---
 .github/workflows/ci.yml   | 11 +++++++++++
 .github/workflows/docs.yml |  5 ++++-
 2 files changed, 15 insertions(+), 1 deletion(-)

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 6166bf3dc..d8ab34fb9 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -187,6 +187,10 @@ jobs:
       - if: runner.os == 'Windows'
         run: .github/wix.ps1
 
+      # Do not run this on forks. It isn't sufficient to check the pull
+      # request info because we might also be on master in a fork. It
+      # seems that you can't stop scheduled jobs from also running in
+      # forks. See https://github.com/orgs/community/discussions/16109.
       - if: runner.os == 'Windows' && github.event.pull_request.head.repo.fork == false && github.repository_owner == 'GaloisInc'
         shell: bash
         env:
@@ -212,6 +216,10 @@ jobs:
           OS_TAG: ${{ matrix.os }}
           ARCH_TAG: ${{ runner.arch }}
 
+      # Do not run this on forks. It isn't sufficient to check the pull
+      # request info because we might also be on master in a fork. It
+      # seems that you can't stop scheduled jobs from also running in
+      # forks. See https://github.com/orgs/community/discussions/16109.
       - if: github.event.pull_request.head.repo.fork == false && github.repository_owner == 'GaloisInc'
         shell: bash
         env:
@@ -413,6 +421,9 @@ jobs:
   build-push-image:
     runs-on: ubuntu-22.04
     needs: [config]
+    # Do not run this on forks. It seems that you can't stop scheduled
+    # jobs from also running in forks. See
+    # https://github.com/orgs/community/discussions/16109.
     if: (github.event_name == 'schedule' || github.event_name == 'workflow_dispatch' || needs.config.outputs.release == 'true') && github.repository_owner == 'GaloisInc'
     strategy:
       fail-fast: false
diff --git a/.github/workflows/docs.yml b/.github/workflows/docs.yml
index 721a8a587..186854191 100644
--- a/.github/workflows/docs.yml
+++ b/.github/workflows/docs.yml
@@ -47,7 +47,10 @@ jobs:
             -p 'python3.withPackages (pp: [pp.sphinx pp.sphinx_rtd_theme])' \
             --run 'make html'
   build-pages-docs:
-    # Do not run this on forks:
+    # Do not run this on forks. It isn't sufficient to check the pull
+    # request info because we might also be on master in a fork. It
+    # seems that you can't stop scheduled jobs from also running in
+    # forks. See https://github.com/orgs/community/discussions/16109.
     if: github.event.pull_request.head.repo.fork == false && github.repository_owner == 'GaloisInc'
     runs-on: ubuntu-latest
     # The public interface should then allow the user to browse the cryptol