Skip to content

Commit

Permalink
update README
Browse files Browse the repository at this point in the history
  • Loading branch information
@Seasawher
Seasawher committed Apr 3, 2024
1 parent 6d5dcaa commit ad04714
Showing 1 changed file with 2 additions and 0 deletions.
2 changes: 2 additions & 0 deletions README.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -19,6 +19,8 @@ Don't forget to run `lake update mdgen` after editing the `lakefile`. And simply

* The comments enclosed with an `/-! ... -/` or `/- ... -/` are converted as ground text.

* Nested block comments can also be handled.

* The inline comment, doc comment and non-comment parts are converted to lean code blocks.

* Lines ending with `--#` are ignored.
Expand Down

0 comments on commit ad04714

Please sign in to comment.