summary refs log tree commit diff
path: root/doc/languages-frameworks/agda.section.md
diff options
context:
space:
mode:
Diffstat (limited to 'doc/languages-frameworks/agda.section.md')
-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 ff3d70ef0c6..cb1f12eec23 100644
--- a/doc/languages-frameworks/agda.section.md
+++ b/doc/languages-frameworks/agda.section.md
@@ -146,7 +146,7 @@ agdaPackages.mkDerivation {
 
 ### Building Agda packages {#building-agda-packages}
 
-The default build phase for `agdaPackages.mkDerivation` simply runs `agda` on the `Everything.agda` file.
+The default build phase for `agdaPackages.mkDerivation` 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.
@@ -250,7 +250,7 @@ Usually, the maintainers will answer within a week or two with a new release.
 Bumping the version of that reverse dependency should be a further commit on your PR.
 
 In the rare case that a new release is not to be expected within an acceptable time,
-simply mark the broken package as broken by setting `meta.broken = true;`.
+mark the broken package as broken by setting `meta.broken = true;`.
 This will exclude it from the build test.
 It can be added later when it is fixed,
 and does not hinder the advancement of the whole package set in the meantime.