max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
lean4-htt/tests/pkg/user_plugin
History
Exact
Mac Malone f8b7f30f5c
fix: change plugin separator to = (#13737) 
This PR changes the separator between the plugin file name and the
initialization function in `--plugin` from `:` to `=`. This prevents
clashes with the `:` in drive prefixes on Windows.
2026-05-15 08:28:21 +00:00
..
clean.sh test: always clean full .lake (#13703) 2026-05-12 16:25:00 +00:00
lakefile.toml
lean-toolchain chore: relative lean-toolchains (#12652) 2026-02-25 10:23:35 +00:00
run_test.sh fix: change plugin separator to = (#13737) 2026-05-15 08:28:21 +00:00
test.lean
testEnv.lean
testEnvUse.lean
UserEnvPlugin.lean
UserPlugin.lean