You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
odoc: Don't add unecessary space in references and links (#2608)
Avoid adding a space before the text of a reference or link:
{{!ref}text}
{{:url}text}
As regular comments might be formatted as docstrings, the space must be
preserved if it appears in the source to avoid crashing.
odoc-parser is changed to preserve this information.
This slightly changes the formatting of references and links:
{{:https://github.com/mirage/irmin/blob/main/README_PPX.md} documentation
- for [ppx_irmin]})*)
+ for [ppx_irmin]})*)
...
- of similar bindings themselves, by using the appropriate {{!Merge.MSet}
- multi-sets}. *)
+ of similar bindings themselves, by using the appropriate
+ {{!Merge.MSet} multi-sets}. *)
0 commit comments