diff options
| author | Daniil Cherednik <[email protected]> | 2022-04-12 14:38:38 +0300 |
|---|---|---|
| committer | Daniil Cherednik <[email protected]> | 2022-04-12 14:38:38 +0300 |
| commit | 70ba69a2375d52936f770c56cc0ca25564316282 (patch) | |
| tree | df27a48fbd3e1323984dfa2ed1e3e03d7e3e5446 | |
| parent | 6aff4cb8c380f6014d13dac9a09cb35278f611c9 (diff) | |
Mark ".github" directory as allowed
| -rwxr-xr-x | .github/check_dirs.sh | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/.github/check_dirs.sh b/.github/check_dirs.sh index 83012853799..ba1e685a377 100755 --- a/.github/check_dirs.sh +++ b/.github/check_dirs.sh @@ -11,6 +11,7 @@ declare -A top_dirs=( [certs/]=1, [cmake/]=1, [.git/]=1, + [.github/]=1, [library/]=1, [tools/]=1, ) |