From ddaf76a401b4b7a9d9e41e31dde0cae4b950cf83 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Thu, 21 Jul 2022 20:27:54 +0200 Subject: [PATCH] chore: remove unused code --- Main.lean | 12 ------------ 1 file changed, 12 deletions(-) diff --git a/Main.lean b/Main.lean index e4f7bd0..2ea998e 100644 --- a/Main.lean +++ b/Main.lean @@ -20,18 +20,6 @@ def getTopLevelModules (p : Parsed) : IO (List String) := do throw $ IO.userError "No topLevelModules provided." pure topLevelModules -def runInitCmd (p : Parsed) : IO UInt32 := do - let topLevelModules ← getTopLevelModules p - let res ← lakeSetup topLevelModules - match res with - | Except.ok _ => - let modules := topLevelModules.map Name.mkSimple - let hierarchy ← loadInit modules - let baseConfig := getSimpleBaseContext hierarchy - htmlOutputSetup baseConfig - pure 0 - | Except.error rc => pure rc - def runSingleCmd (p : Parsed) : IO UInt32 := do let topLevelModules ← getTopLevelModules p let relevantModules := [p.positionalArg! "module" |>.as! String]