patch 8.2.1318: no status badge for Github CI

Problem: No status badge for Github CI. Solution: Add a badge.
2020-07-29 17:34:33 +02:00
parent f9a343f8bd
commit ed3c7e6339
2 changed files with 3 additions and 0 deletions
--- a/src/version.c
+++ b/src/version.c
@@ -754,6 +754,8 @@ static char *(features[]) =

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