Add a description to Discord notification

CakeML · Aug 9, 2024 · 3ac0363 · 3ac0363
1 parent ba8a47d
commit 3ac0363
Showing 1 changed file with 12 additions and 0 deletions.
diff --git a/.github/workflows/pure.yml b/.github/workflows/pure.yml
@@ -206,10 +206,22 @@ jobs:
           "title": "PureCake CI #${{ github.run_number }}: ${{ needs.build.result }}",
           "url": "https://github.com/CakeML/pure/actions/runs/${{ github.run_id }}",
           "color": ${{ needs.build.result == 'success' && 8311585 || 13632027 }},
+          "description": "$DESCRIPTION",
           "fields": [
           {"name": "HOL commit", "inline": true,
            "value": "[${{ needs.build.outputs.hol_short_sha }}](https://github.com/HOL-Theorem-Prover/HOL/commit/${{ needs.build.outputs.hol_sha }})"},
           {"name": "CakeML commit", "inline": true,
            "value": "[${{ needs.build.outputs.cakeml_short_sha }}](https://github.com/CakeML/cakeml/commit/${{ needs.build.outputs.cakeml_sha }})"}]
           }]}'
           ${{ secrets.DISCORD_WEBHOOK }}
+        env:
+          DESCRIPTION: |-
+            ${{
+                github.event_name == 'workflow_dispatch' &&
+                  format('Manually triggered by {0}', github.event.sender.login)
+             || github.event_name == 'pull_request' &&
+                  format('[Pull request #{0}](https://github.com/CakeML/pure/pull/{0})', github.event.number)
+             || github.event_name == 'push' &&
+                  format('Push by {0}', github.event.pusher.username || github.event.pusher.name)
+             || 'Weekly scheduled run'
+            }}