diff options
| author | Jan Macku <jamacku@redhat.com> | 2023-04-06 14:04:14 +0200 |
|---|---|---|
| committer | MartinNowack <2443641+MartinNowack@users.noreply.github.com> | 2023-04-14 15:58:47 +0100 |
| commit | 02b52541c5e8262e7f7a909d90fb898399d822bd (patch) | |
| tree | 77be9b534059c9111a14329e8d66e4f4a2c025e9 /.github | |
| parent | 896c652ed7d91d6ff954463c7c1e4bf95096481b (diff) | |
| download | klee-02b52541c5e8262e7f7a909d90fb898399d822bd.tar.gz | |
ci: run ShellCheck on `*.inc` shell scripts
Diffstat (limited to '.github')
| -rw-r--r-- | .github/workflows/differential-shellcheck.yml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/.github/workflows/differential-shellcheck.yml b/.github/workflows/differential-shellcheck.yml index 2dd92e9b..55bba982 100644 --- a/.github/workflows/differential-shellcheck.yml +++ b/.github/workflows/differential-shellcheck.yml @@ -28,4 +28,5 @@ jobs: uses: redhat-plumbers-in-action/differential-shellcheck@v4 with: severity: warning + include-path: scripts/**.inc token: ${{ secrets.GITHUB_TOKEN }} |