about summary refs log tree commit diff
diff options
context:
space:
mode:
authorCole Helbling <cole.e.helbling@outlook.com>2020-06-17 13:50:59 -0700
committerCole Helbling <cole.e.helbling@outlook.com>2020-06-17 13:51:43 -0700
commit5baa7541d73e57f26d1da9ca0c663cc7be31f256 (patch)
tree5f3188005bb7bf8d73430436ce9cc8f451b0ee1c
parente215c3bcac09ea3c1b1c9a5f9acd65b8e1791133 (diff)
downloadnixlib-5baa7541d73e57f26d1da9ca0c663cc7be31f256.tar
nixlib-5baa7541d73e57f26d1da9ca0c663cc7be31f256.tar.gz
nixlib-5baa7541d73e57f26d1da9ca0c663cc7be31f256.tar.bz2
nixlib-5baa7541d73e57f26d1da9ca0c663cc7be31f256.tar.lz
nixlib-5baa7541d73e57f26d1da9ca0c663cc7be31f256.tar.xz
nixlib-5baa7541d73e57f26d1da9ca0c663cc7be31f256.tar.zst
nixlib-5baa7541d73e57f26d1da9ca0c663cc7be31f256.zip
agda: fix manual build
    /build/doc/manual-full.xml:12764:35: error: ID "build-phase" has already been defined
    /build/doc/manual-full.xml:9029:33: error: first occurrence of ID "build-phase"
-rw-r--r--doc/languages-frameworks/agda.section.md4
1 files changed, 2 insertions, 2 deletions
diff --git a/doc/languages-frameworks/agda.section.md b/doc/languages-frameworks/agda.section.md
index 72b895f5da12..9ce046d05b6f 100644
--- a/doc/languages-frameworks/agda.section.md
+++ b/doc/languages-frameworks/agda.section.md
@@ -67,13 +67,13 @@ A derivation can then be written using `agdaPackages.mkDerivation`. This has sim
 + `libraryName` should be the name that appears in the `*.agda-lib` file, defaulting to `pname`.
 + `libraryFile` should be the file name of the `*.agda-lib` file, defaulting to `${libraryName}.agda-lib`.
 
-### Build phase
+### Building Agda packages
 The default build phase for `agdaPackages.mkDerivation` simply runs `agda` on the `Everything.agda` file.
 If something else is needed to build the package (e.g. `make`) then the `buildPhase` should be overridden.
 Additionally, a `preBuild` or `configurePhase` can be used if there are steps that need to be done prior to checking the `Everything.agda` file.
 `agda` and the Agda libraries contained in `buildInputs` are made available during the build phase.
 
-### Install phase
+### Installing Agda packages
 The default install phase copies agda source files, agda interface files (`*.agdai`) and `*.agda-lib` files to the output directory.
 This can be overridden.