aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac/vernac.mllib
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2017-08-17 16:38:30 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2017-08-17 16:38:30 +0200
commit63da901edc3ab5b69098499cdc01ab50ed9b3353 (patch)
tree0f1c411b9621416ef2720b81430508b619523ff9 /vernac/vernac.mllib
parent7451651a70be86ef8f510faabcba445766595187 (diff)
parent6de02170275e49e5f58a93eb5513d5eb8cb9aa38 (diff)
Merge PR #972: 8.7 change entries
Diffstat (limited to 'vernac/vernac.mllib')
0 files changed, 0 insertions, 0 deletions