fix: print usage when called without arguments

main
Gabriel Ebner 2022-01-20 15:03:10 +01:00
parent 5ed0a8e99f
commit fd5280f30a
1 changed files with 4 additions and 0 deletions

View File

@ -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