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)
2021-08-07 12:32:20 +02:00
parent cbae580283
commit d57a6bd98c
3 changed files with 83 additions and 0 deletions
--- a/src/version.c
+++ b/src/version.c
@@ -755,6 +755,8 @@ static char *(features[]) =

 static int included_patches[] =
 {   /* Add new patch number below this line */
+/**/
+    3302,
 /**/
    3301,
 /**/