test: Use lake test. Retired Makefile #87

Merged
aniva merged 1 commits from misc/test-driver into dev 2024-08-18 12:24:56 -07:00
Owner
Vide https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Example.20of.20lake.20test/near/463144326
aniva added the
category
doc
priority
low
labels 2024-08-18 12:23:53 -07:00
aniva self-assigned this 2024-08-18 12:23:53 -07:00
aniva added 1 commit 2024-08-18 12:23:54 -07:00
aniva merged commit 76765c913c into dev 2024-08-18 12:24:56 -07:00
aniva deleted branch misc/test-driver 2024-08-18 12:24:56 -07:00
Sign in to join this conversation.
No description provided.