lean4-htt/tests/pkg/mod_clash/clean.sh
Mac Malone 687698e79d
test: module clash across packages (#11246)
This PR adds a test that covers importing modules defined in multiple
packages.

Currently, will resolve the module to its first occurrence in the its
search order. However, this will soon change, so this test is designed
to analyze that behavior.
2025-11-19 02:23:34 +00:00

3 lines
129 B
Bash
Executable file

rm -rf .lake lake-manifest.json produced.out
rm -rf depA/.lake depA/lake-manifest.json
rm -rf depB/.lake depB/lake-manifest.json