allow noisy files

Author: eric-wieser

.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: |