ci : avoid manual updates of docs/ops.md (#16663)

This commit is contained in:
Sigbjørn Skjæret 2025-10-19 14:03:25 +02:00 committed by GitHub
parent fcb235b466
commit cec5edbcae
No known key found for this signature in database
GPG Key ID: B5690EEEBB952194
1 changed files with 2 additions and 0 deletions

View File

@ -3,10 +3,12 @@ name: Update Operations Documentation
on:
push:
paths:
- 'docs/ops.md'
- 'docs/ops/**'
- 'scripts/create_ops_docs.py'
pull_request:
paths:
- 'docs/ops.md'
- 'docs/ops/**'
- 'scripts/create_ops_docs.py'