From 5a8251207057208717f62fb8f4b23b172824e5bd Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Wed, 19 Oct 2022 08:22:33 +0530
Subject: [PATCH] Add matcher for make errors (#1457)

---
 .github/make.json             | 16 ++++++++++++++++
 etc/ci/github-actions-make.sh |  2 ++
 2 files changed, 18 insertions(+)
 create mode 100644 .github/make.json

diff --git a/.github/make.json b/.github/make.json
new file mode 100644
index 0000000000..44e117d659
--- /dev/null
+++ b/.github/make.json
@@ -0,0 +1,16 @@
+{
+    "problemMatcher": [
+        {
+            "owner": "make-problem-matcher",
+            "pattern": [
+                {
+                    "regexp": "^make(|\\[\\d+\\]): \\*+ \\[(.*?)o?] (Error) (\\d+)",
+                    "file": 2,
+                    "message": 2,
+                    "severity": 3,
+                    "code": 4
+                }
+            ]
+        }
+    ]
+}
diff --git a/etc/ci/github-actions-make.sh b/etc/ci/github-actions-make.sh
index 2084165408..27419804e7 100755
--- a/etc/ci/github-actions-make.sh
+++ b/etc/ci/github-actions-make.sh
@@ -30,6 +30,8 @@ if [[ "${unameOut}" == CYGWIN* ]]; then
     make_one_time_file_real="--real"
 fi
 
+echo "::add-matcher::.github/make.json"
+
 rm -f finished.ok
 (make "$@" ${OUTPUT_SYNC} TIMED=1 TIMING=1 "${reportify}" 2>&1 && touch finished.ok) | tee -a time-of-build.log
 python "./etc/coq-scripts/timing/make-one-time-file.py" ${make_one_time_file_real} "time-of-build.log" "time-of-build-pretty.log" || exit $?