• Guillaume Melquiond's avatar
    Replace the [...] syntax from why3doc by a Markdown-like syntax. · fee45607
    Guillaume Melquiond authored
    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 delimit code using `` `...` ``".
    fee45607
Name
Last commit
Last update
..
doc_def.ml Loading commit data...
doc_def.mli Loading commit data...
doc_html.ml Loading commit data...
doc_html.mli Loading commit data...
doc_lexer.mll Loading commit data...
doc_main.ml Loading commit data...