Skip to content

Commit 8c312a0

Browse files
nadMatthewDaggitt
authored andcommitted
Turned off the NoEquivWhenSplitting warning.
1 parent 1b61340 commit 8c312a0

File tree

1 file changed

+2
-0
lines changed

1 file changed

+2
-0
lines changed

standard-library.agda-lib

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,2 +1,4 @@
11
name: standard-library-1.7.2
22
include: src
3+
flags:
4+
--warning=noNoEquivWhenSplitting

0 commit comments

Comments
 (0)