Merge branch 'master' into graft

Amber-MD · Aug 18, 2020 · f414ea1 · f414ea1
2 parents 6495ca5 + 53250cf
commit f414ea1
Showing 1 changed file with 5 additions and 0 deletions.
diff --git a/Jenkinsfile b/Jenkinsfile
@@ -109,6 +109,11 @@ pipeline {
                                 """
                             } catch (error) {
                                 echo "PGI BUILD AND/OR TEST FAILED"
+                                try {
+                                    pullRequest.comment("The PGI build in Jenkins failed.")
+                                } catch (err2) {
+                                    echo "Could not post a PR comment: ${err2}"
+                                }
                             }
                         }
                     }