agda/doc/release-notes/2.4.0.1.md

Release notes for Agda 2 version 2.4.0.1

• The option --compile-no-main has been renamed to --no-main.

• COMPILED_DATA pragmas can now be given for records.

• Various bug fixes.