patch 8.2.1735: Github actions appear to timeout too soon

Problem: Github actions appear to timeout too soon. Solution: use "timeout" instead of "ping".
2020-09-23 22:27:22 +02:00
parent 148ce7ae62
commit 851d108313
2 changed files with 4 additions and 2 deletions
--- a/src/version.c
+++ b/src/version.c
@@ -750,6 +750,8 @@ static char *(features[]) =

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