[ #1388 ] Forgotten .err file.

agda · Feb 1, 2016 · 3b8f5ba · 3b8f5ba
1 parent 470dbcf
commit 3b8f5ba
Showing 1 changed file with 2 additions and 0 deletions.
diff --git a/test/Fail/Issue1388.err b/test/Fail/Issue1388.err
@@ -0,0 +1,2 @@
+Issue1388.agda:7,1-19
+No declarations allowed after top-level module.