Skip to content

Commit f5b7fbd

Browse files
plt-amyMatthewDaggitt
plt-amy
authored and
MatthewDaggitt
committed
update NoEquivWhenSplitting warning name
1 parent 8c312a0 commit f5b7fbd

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

‎standard-library.agda-lib‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
11
name: standard-library-1.7.2
22
include: src
33
flags:
4-
--warning=noNoEquivWhenSplitting
4+
--warning=noUnsupportedIndexedMatch

0 commit comments

Comments
 (0)