diff --git a/src/libraries/utils/markdown.ml b/src/libraries/utils/markdown.ml index 4d33aa797e8e178b77b185d6d0bf030f51a265a8..f442f67593537cdc8fba284a2f59127fa9189021 100644 --- a/src/libraries/utils/markdown.ml +++ b/src/libraries/utils/markdown.ml @@ -49,10 +49,10 @@ type block_element = and block = block_element list and table = { - caption: text option; - header: (text * align) list; - content: text list list; - } + caption: text option; + header: (text * align) list; + content: text list list; +} and element = | Comment of string (** markdown comment, printed <!-- like this --> *)