diff --git a/src/Idris/Parser.idr b/src/Idris/Parser.idr index bb106ba..efeeba0 100644 --- a/src/Idris/Parser.idr +++ b/src/Idris/Parser.idr @@ -1519,6 +1519,9 @@ data CmdArg : Type where ||| The command takes an option. OptionArg : CmdArg + ||| The command takes a file. + FileArg : CmdArg + export Show CmdArg where show NoArg = "" @@ -1526,6 +1529,7 @@ Show CmdArg where show ExprArg = "" show NumberArg = "" show OptionArg = "