Limit GitHub comments to 32768 characters. (#8084)

GitHub has a limit of twice that for comments, but 32k should be more than
enough to say what we want to say.

jenkins/Jenkinsfile

@@ -88,6 +88,11 @@ def githubGetPullRequestLabels ()
 
 def githubAddComment (url, markdown)
 {
+    if (markdown.length () > 32768) {
+        // GitHub only allows adding comments < 65536 characters log, so lets cap at half that, which should be more than enough to say that something went horribly wrong
+        markdown = markdown.substring (0, 32768)
+    }
+
     def json = groovy.json.JsonOutput.toJson ([body: markdown])
     def jsonFile = "${workspace}/xamarin-macios/jenkins/commit-comments.json"
     try {

jenkins/add-commit-comment.sh

@@ -71,15 +71,19 @@ fi
 
 JSONFILE=$(mktemp)
 LOGFILE=$(mktemp)
+TMPFILE=$(mktemp)
 cleanup ()
 {
-	rm -f "$JSONFILE" "$LOGFILE"
+	rm -f "$JSONFILE" "$LOGFILE" "$TMPFILE"
 }
 trap cleanup ERR
 trap cleanup EXIT
 
+# Cap comment at 32768 characters, to avoid running into GitHub limits.
+head -c 32768 "$FILE" > "$TMPFILE"
+
 printf '{\n"body": ' > "$JSONFILE"
-python -c 'import json,sys; print(json.dumps(sys.stdin.read()))' < "$FILE" >> "$JSONFILE"
+python -c 'import json,sys; print(json.dumps(sys.stdin.read()))' < "$TMPFILE" >> "$JSONFILE"
 printf '}\n' >> "$JSONFILE"
 
 if test -n "$VERBOSE"; then