Skip to content

Commit

Permalink
correct the docs for the dump-ipkg-json command
Browse files Browse the repository at this point in the history
  • Loading branch information
mattpolzin committed Jun 5, 2024
1 parent be72fdb commit e042713
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion src/Idris/CommandLine.idr
Original file line number Diff line number Diff line change
Expand Up @@ -283,7 +283,7 @@ options = [MkOpt ["--check", "-c"] [] [CheckOnly]
(Just "Interactively initialise a new project"),
MkOpt ["--dump-ipkg-json"] [Optional "package file"]
(\ f => [Package DumpJson f])
(Just "Interactively initialise a new project"),
(Just "Dump an Idris2 package file in the JSON format"),
MkOpt ["--build"] [Optional "package file"]
(\f => [Package Build f])
(Just "Build modules/executable for the given package"),
Expand Down

0 comments on commit e042713

Please sign in to comment.