Commit d736e9d
committed
ci(docs): trigger docs deploy when the deploy scripts change
The Documentation workflow runs dev-tools/docs/mike_deploy.sh and
smoke_check_pages.sh, but its push/PR path filters did not include
dev-tools/docs/**. A fix that touched only those scripts therefore merged
without ever re-running the docs deploy, leaving the live site stale.
Add dev-tools/docs/** to both path filters (and .github/workflows/docs.yml
to the PR filter for parity) so script changes trigger a deploy.1 parent 555f9d1 commit d736e9d
1 file changed
Lines changed: 3 additions & 0 deletions
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
5 | 5 | | |
6 | 6 | | |
7 | 7 | | |
| 8 | + | |
8 | 9 | | |
9 | 10 | | |
10 | 11 | | |
| |||
14 | 15 | | |
15 | 16 | | |
16 | 17 | | |
| 18 | + | |
17 | 19 | | |
18 | 20 | | |
19 | 21 | | |
20 | 22 | | |
| 23 | + | |
21 | 24 | | |
22 | 25 | | |
23 | 26 | | |
| |||
0 commit comments