diff options
| author | dcherednik <[email protected]> | 2023-12-04 17:32:39 +0300 |
|---|---|---|
| committer | dcherednik <[email protected]> | 2023-12-05 04:23:46 +0300 |
| commit | 219d27bd787dc997c608232abc08f9cf0310422c (patch) | |
| tree | 31c7d913bddea5eade444f2af5cf01f30659e7d0 /.github | |
| parent | 729685076fffeae4fcfb8df31b8861813fc4a9be (diff) | |
Add devtools to allowed dirs
Diffstat (limited to '.github')
| -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 a72db06a7a8..6ab47851cb0 100755 --- a/.github/check_dirs.sh +++ b/.github/check_dirs.sh @@ -17,6 +17,7 @@ declare -A top_dirs=( [scripts/]=1, [yt/]=1, [vendor/]=1, + [devtools/]=1, ) cd $GIT_URL |