Skip to content

Commit

Permalink
[ #1346, #4316 ] Added a missing .warn file.
Browse files Browse the repository at this point in the history
  • Loading branch information
@nad
nad committed Feb 23, 2020
1 parent fb44544 commit aa58c68
Showing 1 changed file with 14 additions and 0 deletions.
14 changes: 14 additions & 0 deletions test/Succeed/Issue1346Import.warn
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,14 @@
AGDA_UNEXPECTED_FAIL

ret > ExitFailure 1
out > Issue1346Import.agda:9,11-28
out > Don't know how to parse true ∷ false ∷ []. Could mean any one of:
out > true ∷ (false ∷ [])
out > true ∷ (false ∷ [])
out > true ∷ (false ∷ [])
out > (true ∷ false) ∷ []
out > Operators used in the grammar:
out > ∷ (infixr operator, level 4) [_,_ (Issue1346.agda:14,17-20)]
out > ∷ (infixr operator, level 5) [_∷_ (Issue1346.agda:25,5-8)]
out > when scope checking true ∷ false ∷ []
out >

2 comments on commit aa58c68

@jespercockx
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Is this a mistake? I don't get this error when I run the test suite on my PC (and anyway, there shouldn't be test cases with AGDA_UNEXPECTED_FAIL).

@nad
Copy link
Contributor Author

@nad nad commented on aa58c68 Feb 24, 2020

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

See #1346.

Please sign in to comment.