commit | d57a6bd98c9a57b766eadcc3f10e9c4169c788aa | [log] [tgz] |
---|---|---|
author | Bram Moolenaar <Bram@vim.org> | Sat Aug 07 12:32:20 2021 +0200 |
committer | Bram Moolenaar <Bram@vim.org> | Sat Aug 07 12:32:20 2021 +0200 |
tree | 44f260d08eb82efba55c1993f9cde1d78cefb217 | |
parent | cbae5802832b29f3a1af4cb6b0fc8cf69f17cbf4 [diff] |
patch 8.2.3302: Coverity is not run from github Problem: Coverity is not run from github. Solution: Add a coverity script. (James McCoy, closes #8714)
diff --git a/src/version.c b/src/version.c index 3f5a6f7..6544fd3 100644 --- a/src/version.c +++ b/src/version.c
@@ -756,6 +756,8 @@ static int included_patches[] = { /* Add new patch number below this line */ /**/ + 3302, +/**/ 3301, /**/ 3300,