diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-12-05 09:59:08 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-12-05 09:59:08 +0100 |
| commit | 423b7298535c88b14926e92a8763420c69f89f6d (patch) | |
| tree | 40ed99dd79dffe7e8dd92cb75b124267ee072162 /vernac/classes.ml | |
| parent | 4d62482e8c996024fdcdee1549bb8bfe28961763 (diff) | |
| parent | 195a652e38bcb6f58c156495492999ea8ee4e64e (diff) | |
Merge PR #6301: [vernac] Couple of tweaks missing from previous PRs.
Diffstat (limited to 'vernac/classes.ml')
0 files changed, 0 insertions, 0 deletions