diff options
author | Silvan Mosberger <contact@infinisil.com> | 2019-08-07 13:37:36 +0200 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-08-07 13:37:36 +0200 |
commit | dd7de2d096818ec2ebc1089af0e1a3f09b3288f8 (patch) | |
tree | 1599c15b1d923d385ae2ec4b78d9a3ae1fcf9902 /doc/languages-frameworks | |
parent | 25e47152b140eb702051c2267e72373b0d735095 (diff) | |
parent | 349a843ef413f9746ce97625328670451d5574c0 (diff) |
add options for build idris package (#65666)
add options for build idris package
Diffstat (limited to 'doc/languages-frameworks')
-rw-r--r-- | doc/languages-frameworks/idris.section.md | 18 |
1 files changed, 18 insertions, 0 deletions
diff --git a/doc/languages-frameworks/idris.section.md b/doc/languages-frameworks/idris.section.md index 3025172b5c981..e88015f08e3f8 100644 --- a/doc/languages-frameworks/idris.section.md +++ b/doc/languages-frameworks/idris.section.md @@ -124,3 +124,21 @@ in another file (say `default.nix`) to be able to build it with ``` $ nix-build -A yaml ``` + +## Passing options to `idris` commands + +The `build-idris-package` function provides also optional input values to set additional options for the used `idris` commands. + +Specifically, you can set `idrisBuildOptions`, `idrisTestOptions`, `idrisInstallOptions` and `idrisDocOptions` to provide additional options to the `idris` command respectively when building, testing, installing and generating docs for your package. + +For example you could set + +``` +build-idris-package { + idrisBuildOptions = [ "--log" "1" "--verbose" ] + + ... +} +``` + +to require verbose output during `idris` build phase. |