From ecacf2107c5c56f94810c4f1eeedf6ac8bb153ec Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Wed, 6 Mar 2024 15:27:22 -0800 Subject: [PATCH] feat(build): Add shared facet for lean_lib --- lakefile.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/lakefile.lean b/lakefile.lean index f0832e2..89ad70f 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -4,6 +4,7 @@ open Lake DSL package pantograph lean_lib Pantograph { + defaultFacets := #[LeanLib.sharedFacet] } @[default_target]