6 Commits

Author	SHA1	Message	Date
Ryan Mulligan	b8344f9e5c	doc: explicit Markdown anchors for top-level headings; remove metadata ... I used the existing anchors generated by Docbook, so the anchor part should be a no-op. This could be useful depending on the infrastructure we choose to use, and it is better to be explicit than rely on Docbook's id generating algorithms. I got rid of the metadata segments of the Markdown files, because they are outdated, inaccurate, and could make people less willing to change them without speaking with the author.	2021-01-01 10:02:57 -08:00
Manuel Bärenz	87cab901a3	agda.section.md: Fix header, enumerations, capitalisation	2020-09-18 12:42:06 +02:00
Cole Helbling	5baa7541d7	agda: fix manual build ... /build/doc/manual-full.xml:12764:35: error: ID "build-phase" has already been defined /build/doc/manual-full.xml:9029:33: error: first occurrence of ID "build-phase"	2020-06-17 13:51:43 -07:00
Alex Rice	e215c3bcac	agda: install literate files	2020-06-01 13:59:20 +01:00
Uma Zalakain	196cc47005	agda: fix typo in library management documentation ... Agda expects a "depend" (not "depends") field in the library description.	2020-05-24 14:20:05 +02:00
Alex Rice	d30e2468e0	agda: rework builder	2020-05-14 20:54:11 +01:00