diff options
| author | Ryan Mulligan <ryan@ryantm.com> | 2021-01-01 09:45:43 -0800 |
|---|---|---|
| committer | Ryan Mulligan <ryan@ryantm.com> | 2021-01-01 10:02:57 -0800 |
| commit | b8344f9e5cd2dcd21e31d1c077393bdc7b19e860 (patch) | |
| tree | 55581aab77e702b4403624728ced282c72bf4609 /doc/languages-frameworks/agda.section.md | |
| parent | 70a061bd6c5ff08c0f540e5f06cd1e91b717ce25 (diff) | |
| download | nixpkgs-b8344f9e5cd2dcd21e31d1c077393bdc7b19e860.tar nixpkgs-b8344f9e5cd2dcd21e31d1c077393bdc7b19e860.tar.gz nixpkgs-b8344f9e5cd2dcd21e31d1c077393bdc7b19e860.tar.bz2 nixpkgs-b8344f9e5cd2dcd21e31d1c077393bdc7b19e860.tar.lz nixpkgs-b8344f9e5cd2dcd21e31d1c077393bdc7b19e860.tar.xz nixpkgs-b8344f9e5cd2dcd21e31d1c077393bdc7b19e860.tar.zst nixpkgs-b8344f9e5cd2dcd21e31d1c077393bdc7b19e860.zip | |
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.
Diffstat (limited to 'doc/languages-frameworks/agda.section.md')
| -rw-r--r-- | doc/languages-frameworks/agda.section.md | 7 |
1 files changed, 1 insertions, 6 deletions
diff --git a/doc/languages-frameworks/agda.section.md b/doc/languages-frameworks/agda.section.md index 5ba4e285f42..66b4a208302 100644 --- a/doc/languages-frameworks/agda.section.md +++ b/doc/languages-frameworks/agda.section.md @@ -1,9 +1,4 @@ ---- -title: Agda -author: Alex Rice (alexarice) -date: 2020-01-06 ---- -# Agda +# Agda {#agda} ## How to use Agda |