aboutsummaryrefslogtreecommitdiff
path: root/kernel/type_errors.ml
diff options
context:
space:
mode:
authorClément Pit-Claudel2018-09-25 10:43:42 +0200
committerThéo Zimmermann2018-09-25 12:45:57 +0200
commit44e9654d053b72931866d61b859ba831982c14fd (patch)
tree998e0f99cd7f7642c8ea6cd3cf0beed03a0598c1 /kernel/type_errors.ml
parent7eb8a7eb8d23ffaf149f71a46fb1b089b90db7f8 (diff)
[doc] Fix GH-8529: wrap macro definitions in math delimiters for MathJax
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions