mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-01 01:09:03 +03:00
59460c2f46
* [ admin ] Update CHANGELOG and CONTRIBUTORS We really need to do a release at some point... * [ ci ] Don't check capitalised proper names in links and code Sometimes hyperlinks and code-blocks just don't use the "proper" capitalisation (e.g. `.html` vs `.HTML`), and that's okay. (or even critical as links may not be found without "incorrect" format) * [ ci ] Don't check terminology in links and code-blocks Hopefully this is the right fix for the problem in #2703 * [ ci ] 3rd attempt at fixing nl linter * [ ci ] Attempt no. 4 at fixing nl linter * [ ci ] Point NL linter at YAML config file Was that actually it?? * Update CHANGELOG.md * Add note about forward declaration of records * [ admin ] Add PR template with CHANGELOG reminder To hopefully help mitigate big crawl-throughs of what's changed, à la #2703. * [ admin ] Reflow CHANGELOG to 80 characters where possible Only done for the "next version" changes for the sake of diff size. (Personally, I'd want to have the linter enforce this, but that might be too extreme; there's already a note in the CI config complaining about line length...) * [ admin ] Make linter happy It never ends... Co-authored-by: Joel Berkeley <16429957+joelberkeley@users.noreply.github.com> Co-authored-by: Steve Dunham <dunhamsteve@gmail.com>
44 lines
1.2 KiB
YAML
44 lines
1.2 KiB
YAML
---
|
|
###########################
|
|
###########################
|
|
## Markdown Linter rules ##
|
|
###########################
|
|
###########################
|
|
|
|
# Linter rules doc:
|
|
# - https://github.com/DavidAnson/markdownlint
|
|
#
|
|
# Note:
|
|
# To comment out a single error:
|
|
# <!-- markdownlint-disable -->
|
|
# any violations you want
|
|
# <!-- markdownlint-restore -->
|
|
#
|
|
|
|
###############
|
|
# Rules by id #
|
|
###############
|
|
MD001: false
|
|
MD003: false
|
|
MD004: false # Unordered list style
|
|
MD007:
|
|
indent: 2 # Unordered list indentation
|
|
MD013:
|
|
line_length: 400 # Line length 80 is far to short
|
|
MD024:
|
|
siblings_only: true # allow duplicate headings in CHANGELOG
|
|
MD026:
|
|
punctuation: ".,;:。，；:" # List of not allowed
|
|
MD029: false # Ordered list item prefix
|
|
MD033: false # Allow inline HTML
|
|
MD036: false # Emphasis used instead of a heading
|
|
MD044: # Proper names should have the correct capitalization
|
|
code_blocks: false
|
|
html_elements: false
|
|
MD046: false # Idented code block instead of fenced off
|
|
|
|
#################
|
|
# Rules by tags #
|
|
#################
|
|
blank_lines: false # Error on blank lines
|