add test that exercises new installdir command

idris-lang · Sep 11, 2024 · 1787664 · 1787664
1 parent 2560acb
commit 1787664
Show file tree

Hide file tree

Showing 4 changed files with 24 additions and 0 deletions.
diff --git a/tests/idris2/pkg/pkg020/expected b/tests/idris2/pkg/pkg020/expected
@@ -0,0 +1,2 @@
+/idris2-0.7.0/test-0.3.0
+/idris2-0.7.0
diff --git a/tests/idris2/pkg/pkg020/run b/tests/idris2/pkg/pkg020/run
@@ -0,0 +1,9 @@
+. ../../../testutils.sh
+
+# pretend Idris2 is installed at root for reproducible
+# installdirs:
+IDRIS2_PREFIX=/ idris2 --dump-installdir test.ipkg
+
+# by contrast, the location containing all installed packages:
+IDRIS2_PREFIX=/ idris2 --libdir
+
diff --git a/tests/idris2/pkg/pkg020/src/Stuff.idr b/tests/idris2/pkg/pkg020/src/Stuff.idr
@@ -0,0 +1,5 @@
+module Stuff
+
+export
+say : String
+say = "Stuff"
diff --git a/tests/idris2/pkg/pkg020/test.ipkg b/tests/idris2/pkg/pkg020/test.ipkg
@@ -0,0 +1,8 @@
+package test
+version = 0.3.0
+
+-- modules to install
+modules = Stuff
+
+sourcedir = "src"
+