mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-24 12:14:26 +03:00
15 lines
331 B
Plaintext
15 lines
331 B
Plaintext
|
########################
|
||
|
|
########################
|
||
|
|
## LaTeX Linter rules ##
|
||
|
|
########################
|
||
|
|
########################
|
||
|
|
|
||
|
|
CmdLine {
|
||
|
|
# Command terminated with space.
|
||
|
|
--nowarn 1
|
||
|
|
|
||
|
|
# You ought to remove spaces in front of punctuation.
|
||
|
|
# This gets confused in code blocks, failing on eg. `x : Nat`
|
||
|
|
--nowarn 26
|
||
|
|
}
|