From 45c18ad79c5cd28dcf8f29ba99e32720dc02ab45 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 9 Dec 2019 16:55:51 -0800
Subject: [PATCH] chore: make sure we fail test if there are errors

---
 tests/lean/run/frontend1.lean | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/tests/lean/run/frontend1.lean b/tests/lean/run/frontend1.lean
index 8ccdc509fd..22a4620c1e 100644
--- a/tests/lean/run/frontend1.lean
+++ b/tests/lean/run/frontend1.lean
@@ -2,11 +2,13 @@ import Init.Lean.Elab
 open Lean
 open Lean.Elab
 
+
 def run (input : String) : MetaIO Unit :=
 do env  ← MetaIO.getEnv;
    opts ← MetaIO.getOptions;
    let (env, messages) := process input env opts;
    messages.toList.forM $ fun msg => IO.println msg;
+   when messages.hasErrors $ throw (IO.userError "errors have been found");
    pure ()
 
 def test := IO Unit