merge: rewrite-docs
I've omitted docs/*.org from this merge, as there is still work left to do there, but I am pushing the module docs early so folks can benefit from the new docs sooner.
This commit is contained in:
commit
1f8bf7accb
179 changed files with 13125 additions and 8630 deletions
|
@ -1,4 +1,57 @@
|
|||
#+TITLE: :lang agda
|
||||
# -*- mode: doom-docs-org -*-
|
||||
#+title: :lang agda
|
||||
#+subtitle: Types of types of types of types...
|
||||
#+created: August 21, 2018
|
||||
#+since: 21.12.0 (#821)
|
||||
|
||||
* Description :unfold:
|
||||
This module adds support for the [[http://wiki.portal.chalmers.se/agda/pmwiki.php][agda]] programming language. The Emacs support
|
||||
exists directly in the agda repository but not in melpa.
|
||||
exists directly in the agda repository, but not in melpa.
|
||||
|
||||
** Maintainers
|
||||
/This module has no dedicated maintainers./ [[doom-contrib-maintainer:][Become a maintainer?]]
|
||||
|
||||
** Module flags
|
||||
- +local ::
|
||||
Use the =agda-mode= executable that comes with your local =agda= install.
|
||||
- +tree-sitter ::
|
||||
Leverages tree-sitter for better syntax highlighting and structural text
|
||||
editing. Requires [[doom-module:][:tools tree-sitter]].
|
||||
|
||||
** Packages
|
||||
- unless [[doom-module:][+local]]
|
||||
- [[doom-package:][agda-input]]
|
||||
- [[doom-package:][agda2-mode]]
|
||||
|
||||
** Hacks
|
||||
/No hacks documented for this module./
|
||||
|
||||
** TODO Changelog
|
||||
# This section will be machine generated. Don't edit it by hand.
|
||||
/This module does not have a changelog yet./
|
||||
|
||||
* Installation
|
||||
[[id:01cffea4-3329-45e2-a892-95a384ab2338][Enable this module in your ~doom!~ block.]]
|
||||
|
||||
/This module has no external requirements./
|
||||
|
||||
* TODO Usage
|
||||
#+begin_quote
|
||||
🔨 This module has no usage documentation yet. [[doom-contrib-module:][Write some?]]
|
||||
#+end_quote
|
||||
|
||||
* TODO Configuration
|
||||
#+begin_quote
|
||||
🔨 This module has no configuration documentation yet. [[doom-contrib-module:][Write some?]]
|
||||
#+end_quote
|
||||
|
||||
* Troubleshooting
|
||||
/There are no known problems with this module./ [[doom-report:][Report one?]]
|
||||
|
||||
* Frequently asked questions
|
||||
/This module has no FAQs yet./ [[doom-suggest-faq:][Ask one?]]
|
||||
|
||||
* TODO Appendix
|
||||
#+begin_quote
|
||||
🔨 This module has no appendix yet. [[doom-contrib-module:][Write one?]]
|
||||
#+end_quote
|
||||
|
|
Loading…
Add table
Add a link
Reference in a new issue