Merge pull request 'ci: fix double CI runs on PR pushes' (#75) from fix/ci-double-trigger into main
CI / lint (push) Successful in 7s
CI / sanitizers (address) (push) Successful in 14s
CI / sanitizers (undefined) (push) Successful in 14s
CI / fuzz-build (push) Successful in 14s
CI / build-and-test (push) Successful in 55s
CI / coverage (push) Successful in 11s
CI / valgrind (push) Successful in 12s
CI / lint (push) Successful in 7s
CI / sanitizers (address) (push) Successful in 14s
CI / sanitizers (undefined) (push) Successful in 14s
CI / fuzz-build (push) Successful in 14s
CI / build-and-test (push) Successful in 55s
CI / coverage (push) Successful in 11s
CI / valgrind (push) Successful in 12s
Reviewed-on: #75
This commit was merged in pull request #75.
This commit is contained in:
@@ -1,6 +1,9 @@
|
||||
name: CI
|
||||
|
||||
on: [push, pull_request]
|
||||
on:
|
||||
push:
|
||||
branches: [main]
|
||||
pull_request:
|
||||
|
||||
jobs:
|
||||
lint:
|
||||
|
||||
+2
-1
@@ -1,10 +1,11 @@
|
||||
{
|
||||
"$schema": "https://opencode.ai/config.json",
|
||||
"instructions": ["AGENTS.md"],
|
||||
"permission": {
|
||||
"bash": {
|
||||
"*": "allow",
|
||||
"git push origin main": "deny",
|
||||
"git push main": "ask"
|
||||
"git push main": "deny"
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
Reference in New Issue
Block a user