From e684179ff9c582495b720c3b1310e0648ca24a58 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Fri, 6 Oct 2023 12:13:38 +0200 Subject: Generate the Traits test files for Lean --- tests/lean/lakefile.lean | 1 + 1 file changed, 1 insertion(+) (limited to 'tests/lean/lakefile.lean') diff --git a/tests/lean/lakefile.lean b/tests/lean/lakefile.lean index cc63c48f..1747c581 100644 --- a/tests/lean/lakefile.lean +++ b/tests/lean/lakefile.lean @@ -18,3 +18,4 @@ package «tests» {} @[default_target] lean_lib paper @[default_target] lean_lib poloniusList @[default_target] lean_lib array +@[default_target] lean_lib traits -- cgit v1.2.3