How to use README files?

[shhyou]

How to use README files? I need to add a top-level .agda-lib files, for otherwise I got this error

The name of the top level module does not match the file name. The
module README should be defined in one of the following files:
...paths...

The only notes I found are in HACKING.md which says changing include: src to include: src . in standard-library.agda-lib.

Would it be more helpful to make READMEs an .agda-lib or add instructions to installation-guide.md?

[gallais]

Is this #1743?

[shhyou]

You're right! Closing as (sort of) duplicate.

I want to add that the current issue is about end users who install Agda, perhaps using platform-specific package managers that bundle the standard library together with Agda. In this case having to manually fix the location of READMEs or fix the include path in .agda-lib isn't ideal.