diff --git a/tests/idris2/error/error030/Issue1236.idr b/tests/idris2/error/error030/Issue1236.idr new file mode 100644 index 000000000..81c44dce7 --- /dev/null +++ b/tests/idris2/error/error030/Issue1236.idr @@ -0,0 +1,5 @@ +private +data Foo : Type + +public export +data Foo : Type where diff --git a/tests/idris2/error/error030/expected b/tests/idris2/error/error030/expected new file mode 100644 index 000000000..412228a23 --- /dev/null +++ b/tests/idris2/error/error030/expected @@ -0,0 +1,7 @@ +1/1: Building Issue1236 (Issue1236.idr) +Warning: Main.Foo has been forward-declared with private visibility, cannot change to public export. This will be an error in a later release. + +Issue1236:4:1--5:22 + 4 | public export + 5 | data Foo : Type where + diff --git a/tests/idris2/error/error030/run b/tests/idris2/error/error030/run new file mode 100755 index 000000000..e68088a33 --- /dev/null +++ b/tests/idris2/error/error030/run @@ -0,0 +1,3 @@ +. ../../../testutils.sh + +check Issue1236.idr