Skip to content

Commit b43e457

Browse files
authored
Mention the new feature agda --setup in Agda 2.8.0
1 parent 8ae546d commit b43e457

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

README.md

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -18,7 +18,7 @@ You need to specify a handful of configurations for it to work correctly:
1818

1919
- **The global config directory**: The value can be obtained via flag `--print-agda-app-dir`, serving as the source of Agda's [library management system](https://agda.readthedocs.io/en/latest/tools/package-system.html#package-system). The default path is `$HOME/.config/agda`, and you can override with the enviroment variable `AGDA_DIR`.
2020

21-
- **Built-in library path**: The value can be obtained via flag `--print-agda-data-dir`, but you can override it with the environment variable `Agda_datadir`. It must contain a directory structure `lib/prim/Agda/...`. The content can be copied from Agda's source tree under `src/data` or from the Docker image. \
21+
- **Built-in library path**: The value can be obtained via flag `--print-agda-data-dir`, but you can override it with the environment variable `Agda_datadir`. It must contain a directory structure `lib/prim/Agda/...`. The content can be copied from Agda's source tree under `src/data` or from the Docker image or be populated with [`agda --setup`](https://agda.readthedocs.io/en/v2.8.0/tools/command-line-options.html#cmdoption-setup) (requires Agda v2.8.0+). \
2222
Tip: The minimal requirement to run Agda is these three files (`lib/prim/`) `agda-builtins.agda-lib`, `Agda/Primitive.agda` and `Agda/Primitive/Cubical.agda`.
2323

2424
### Quirks of interaction mode

0 commit comments

Comments
 (0)