Skip to content

Commit

Permalink
[ admin ] update README-related instructions
Browse files Browse the repository at this point in the history
  • Loading branch information
gallais committed Oct 26, 2023
1 parent dd6cf79 commit ad47e19
Showing 1 changed file with 8 additions and 17 deletions.
25 changes: 8 additions & 17 deletions HACKING.md
Original file line number Diff line number Diff line change
Expand Up @@ -244,23 +244,14 @@ you are never committing anything with a whitespace violation:
Type-checking the README directory
----------------------------------

* By default the README directory is not exported in the
`standard-library.agda-lib` file in order to avoid clashing with other people's
README files. This means that by default type-checking a file in the README
directory fails.

* If you wish to type-check a README file, then you will need to change the line:
```
include: src
```
to
```
include: src .
```
in the `standard-library.agda-lib` file.

* Please do not include this change in your pull request.

* By default the README files are not exported in the
`standard-library.agda-lib` file in order to avoid
clashing with other people's README files.

* If you wish to type-check a README file, then you will
need to change the present working directory to `doc/`
where an appropriate `standard-library-doc.agda-lib`
file is present.

Continuous Integration (CI)
===========================
Expand Down

0 comments on commit ad47e19

Please sign in to comment.