Add matcher for make errors (#1457)

mit-plv · Oct 19, 2022 · 5a82512 · 5a82512
1 parent de19418
commit 5a82512
Show file tree

Hide file tree

Showing 2 changed files with 18 additions and 0 deletions.
diff --git a/.github/make.json 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
@@ -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 $?