mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-20 01:41:44 +03:00
Merge pull request #2685 from stefan-hoeck/node_arg
This commit is contained in:
commit
a1ad258e0e
@ -133,6 +133,8 @@
|
||||
now transformer argument is the last, as in the other standard transformers, like `ReaderT` and `StateT`.
|
||||
* Adds `Data.Fin.finToNatEqualityAsPointwise`,
|
||||
which takes a witness of `finToNat k = finToNat l` and proves `k ~~~ l`.
|
||||
* Drop first argument (path to the `node` executable) from `System.getArgs` on
|
||||
the Node.js backend to make it consistent with other backends.
|
||||
|
||||
#### Test
|
||||
|
||||
|
@ -58,15 +58,22 @@ usleep : HasIO io => (usec : Int) -> So (usec >= 0) => io ()
|
||||
usleep usec = primIO (prim__usleep usec)
|
||||
|
||||
-- Get the number of arguments
|
||||
-- Note: node prefixes the list of command line arguments
|
||||
-- with the path to the `node` executable. This is
|
||||
-- inconsistent with other backends, which only list
|
||||
-- the path to the running program. For reasons of
|
||||
-- consistency across backends, this first argument ist
|
||||
-- dropped on the node backend.
|
||||
%foreign "scheme:blodwen-arg-count"
|
||||
supportC "idris2_getArgCount"
|
||||
"node:lambda:() => process.argv.length"
|
||||
"node:lambda:() => process.argv.length - 1"
|
||||
prim__getArgCount : PrimIO Int
|
||||
|
||||
-- Get argument number `n`
|
||||
-- Get argument number `n`. See also `prim__getArgCount`
|
||||
-- about the special treatment of the node backend.
|
||||
%foreign "scheme:blodwen-arg"
|
||||
supportC "idris2_getArg"
|
||||
"node:lambda:n => process.argv[n]"
|
||||
"node:lambda:n => process.argv[n + 1]"
|
||||
prim__getArg : Int -> PrimIO String
|
||||
|
||||
||| Retrieve the arguments to the program call, if there were any.
|
||||
|
@ -4,4 +4,4 @@ import Data.List
|
||||
import System
|
||||
|
||||
main : IO ()
|
||||
main = getArgs >>= (putStrLn . show . drop 2)
|
||||
main = getArgs >>= (putStrLn . show . drop 1)
|
||||
|
Loading…
Reference in New Issue
Block a user