max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: make sure we fail test if there are errors

Browse source
This commit is contained in:
Leonardo de Moura 2019-12-09 16:55:51 -08:00
parent 124ad70bfe
commit 45c18ad79c
1 changed files with 2 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
tests/lean/run/frontend1.lean
View file

@ -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