Mentions légales du service

Skip to content

Replace the [...] syntax from why3doc by a Markdown-like syntax (fix issue #132).

Guillaume Melquiond requested to merge why3doc-markdown into master

Some why3doc comments in the gallery contains [i,j[, which breaks the documentation since it opens a code block that is never closed. The proper way to write it is [\[i,j\[], which is not only ugly but also error-prone.

This commit introduces a Markdown-like syntax for embedded code. It uses the backtick as a delimiter: `[i,j[`. It also supports multi-backticks: you can output `code` using `` `code` ``.

Merge request reports