From cc03a4cb3bb1abec80212a32bae7d905c6cd075e Mon Sep 17 00:00:00 2001 From: Edwin Brady Date: Sun, 28 Jun 2020 22:28:56 +0100 Subject: [PATCH] Add missing test file Apparently I forgot the input for linear012. Oops! --- tests/idris2/linear012/input | 4 ++++ 1 file changed, 4 insertions(+) create mode 100644 tests/idris2/linear012/input diff --git a/tests/idris2/linear012/input b/tests/idris2/linear012/input new file mode 100644 index 000000000..543a43b79 --- /dev/null +++ b/tests/idris2/linear012/input @@ -0,0 +1,4 @@ +:t foo1h +:t foo2h +:t foo3h +:q