[hotfix] remove Issue145 from failing tests

agda · Mar 15, 2024 · edf846a · edf846a
1 parent f73415a
commit edf846a
Showing 1 changed file with 0 additions and 1 deletion.
diff --git a/test/AllFailTests.agda b/test/AllFailTests.agda
@@ -27,7 +27,6 @@ import Fail.QualifiedRecordProjections
 import Fail.NewTypeTwoFields
 import Fail.InvalidName
 import Fail.Issue185
-import Fail.Issue145
 import Fail.ExplicitInstance
 import Fail.ClashingImport
 import Fail.Copatterns