From 8c3b423f64f399c2b5b75d2e6873d103e1a8742a Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Wed, 10 Aug 2022 15:25:24 +0000
Subject: [PATCH] allow noisy files

---
 .github/workflows/lean_build.yml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/.github/workflows/lean_build.yml b/.github/workflows/lean_build.yml
index ad852282f..36bd2945c 100644
--- a/.github/workflows/lean_build.yml
+++ b/.github/workflows/lean_build.yml
@@ -50,7 +50,9 @@ jobs:
 
     - name: Build
       run: |
-        lean --json --make src | python3 _target/deps/mathlib/scripts/detect_errors.py
+        set -o pipefail
+        # TODO: allow noisy files in a better way
+        lean --json --make src | (python3 _target/deps/mathlib/scripts/detect_errors.py || true)
 
     - name: Save olean cache
       run: |