From 4934104eaf879d56cdfbf14c50eaca4cf7539371 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Fri, 13 May 2022 11:55:44 +0200 Subject: [PATCH] chore: update script/reformat.lean --- script/reformat.lean | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/script/reformat.lean b/script/reformat.lean index 403abd752a..54cf2b7e52 100644 --- a/script/reformat.lean +++ b/script/reformat.lean @@ -59,10 +59,11 @@ def parseModule (input : String) (fileName : String) (opts : Options := {}) (tru pure {env, currNamespace, openDecls, stx} | _ => failWith "unknown info tree" - #[{ env := env0, stx := header : CommandSyntax }] ++ topLevelCmds + return #[{ env := env0, stx := header : CommandSyntax }] ++ topLevelCmds unsafe def main (args : List String) : IO Unit := do - let [fileName] ← args | failWith "Usage: reformat file" + let [fileName] := args | failWith "Usage: reformat file" + initSearchPath (← findSysroot) let input ← IO.FS.readFile fileName let moduleStx ← parseModule input fileName let leadingUpdated := mkNullNode (moduleStx.map (·.stx)) |>.updateLeading |>.getArgs