From fd5280f30a1a41a52ac355b10a6c387a1363a490 Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Thu, 20 Jan 2022 15:03:10 +0100 Subject: [PATCH] fix: print usage when called without arguments --- Main.lean | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/Main.lean b/Main.lean index 7f527a4..13e530b 100644 --- a/Main.lean +++ b/Main.lean @@ -4,6 +4,10 @@ import Lean open DocGen4 Lean IO def main (args : List String) : IO Unit := do + if args.isEmpty then + IO.println "Usage: doc-gen4 root/url/ Module1 Module2 ..." + IO.Process.exit 1 + return let root := args.head! let modules := args.tail! let path ← lakeSetupSearchPath (←getLakePath) modules.toArray