Lean -o confusing error message

Stream: lean4

[Eric Wieser]

What is this error message telling me to do?

$ ~/.elan/bin/lean -o Mathlib/Algebra/Ring/Pi.lean
Expected exactly one file name

[Patrick Massot]

Maybe Mac applied his favorite rounding convention as discussed in https://leanprover.zulipchat.com/#narrow/stream/341532-lean4-dev/topic/.5BRFC.5D.20Int.2Ediv.20convention.

[Reid Barton]

I think -o is expecting the output file name

[Mac]

@Eric Wieser As Reid notes, -o consumes a single argument (the output filename), which means lean is left with no file names to process, hence the error. The same error occurs if you run lean without any arguments.