mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-26 05:01:34 +03:00
Make reference and source agree about literate markdown
This commit is contained in:
parent
1e780615b6
commit
59dceb857f
@ -52,4 +52,4 @@ CommonMark
|
|||||||
|
|
||||||
Only code blocks denoted by standard code blocks labelled as idris are recognised.
|
Only code blocks denoted by standard code blocks labelled as idris are recognised.
|
||||||
|
|
||||||
We treat files with an extension of ``.md`` and ``.markdown`` as org-mode style literate files.
|
We treat files with an extension of ``.md`` and ``.markdown`` as CommonMark style literate files.
|
||||||
|
@ -24,7 +24,7 @@ styleOrg = MkLitStyle
|
|||||||
|
|
||||||
export
|
export
|
||||||
styleCMark : LiterateStyle
|
styleCMark : LiterateStyle
|
||||||
styleCMark = MkLitStyle [("```idris", "```")] Nil [".md"]
|
styleCMark = MkLitStyle [("```idris", "```")] Nil [".md", ".markdown"]
|
||||||
|
|
||||||
export
|
export
|
||||||
isLitFile : String -> Maybe LiterateStyle
|
isLitFile : String -> Maybe LiterateStyle
|
||||||
|
Loading…
Reference in New Issue
Block a user