From 4a7c5e214ad15d7099e6b2d6315992e331b149e0 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Fri, 12 Aug 2022 23:04:36 +0200 Subject: [PATCH] chore: drop unused import I didn't even know one could import modules from executables! Not sure how to feel about that. --- lakefile.lean | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/lakefile.lean b/lakefile.lean index e73161f..2e03811 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -1,5 +1,4 @@ import Lake -import Lake.CLI.Main open System Lake DSL package «doc-gen4» @@ -114,4 +113,4 @@ library_facet docs (lib) : FilePath := do let traces ← staticFiles.mapM computeTrace let indexTrace := mixTraceArray traces - return (dataFile, trace.mix indexTrace) \ No newline at end of file + return (dataFile, trace.mix indexTrace)