Skip to content

[ bug ] README text #2910

@jamesmckinna

Description

@jamesmckinna

Issue #1743 and its closing PR #2184 missed updating the following text:

agda-stdlib/doc/README.agda

Lines 289 to 292 in 99167f7

-- Note that all library sources are located under src or ffi. The
-- modules README, README.* and Everything are not really part of the
-- library, so these modules are located in the top-level directory
-- instead.

which should (since v2.0!) instead read:

-- Note that all library sources are located under src or ffi. The
-- modules README, README.* and Everything are not really part of the
-- library, so these modules are located in the doc directory instead.

Metadata

Metadata

Assignees

No one assigned

    Type

    No type

    Projects

    No projects

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions