[ re #2202 ] Additional test file

idris-lang · Jan 11, 2022 · 6380d0f · 6380d0f
1 parent 63ece75
commit 6380d0f
Show file tree

Hide file tree

Showing 3 changed files with 2 additions and 1 deletion.
diff --git a/tests/idris2/perf2202/Church.idr b/tests/idris2/perf2202/Church.idr
diff --git a/tests/idris2/perf2202/expected b/tests/idris2/perf2202/expected
@@ -1 +1,2 @@
 1/1: Building many10000 (many10000.idr)
+1/1: Building Church (Church.idr)
diff --git a/tests/idris2/perf2202/run b/tests/idris2/perf2202/run
@@ -1,4 +1,4 @@
 rm -rf build
 
 $1 --no-color --console-width 0 --check many10000.idr
-
+$1 --no-color --console-width 0 --check Church.idr
Original file line number	Diff line number	Diff line change
		@@ -1 +1,2 @@
		1/1: Building many10000 (many10000.idr)
		1/1: Building Church (Church.idr)