diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2018-06-04 16:29:05 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2018-06-04 16:29:05 +0200 |
| commit | 1136dde7b523047e6091d6e6decb45183e42fc21 (patch) | |
| tree | 777398203b608661f5c6c55ddab4cb20e8ff81b0 /vernac/ppvernac.ml | |
| parent | f9e94fdcf74af274cb85be594ccfd353a63b048a (diff) | |
| parent | 1ecd8d9bfca2863a86adc833d634c3f02fdc14a8 (diff) | |
Merge PR #7601: Fix notation for code snippet in documentation
Diffstat (limited to 'vernac/ppvernac.ml')
0 files changed, 0 insertions, 0 deletions