diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/languages-frameworks/agda.section.md | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/doc/languages-frameworks/agda.section.md b/doc/languages-frameworks/agda.section.md index def9e1254e4..775a7a1a642 100644 --- a/doc/languages-frameworks/agda.section.md +++ b/doc/languages-frameworks/agda.section.md @@ -235,6 +235,13 @@ In a pull request updating e.g. the standard library, you should write the follo This will build all reverse dependencies of the standard library, for example `agdaPackages.agda-categories`, or `agdaPackages.generic`. +In some cases it is useful to build _all_ Agda packages. +This can be done with the following Github comment: + +``` +@ofborg build agda.passthru.tests.allPackages +``` + Sometimes, the builds of the reverse dependencies fail because they have not yet been updated and released. You should drop the maintainers a quick issue notifying them of the breakage, citing the build error (which you can get from the ofborg logs). |