aboutsummaryrefslogtreecommitdiffhomepage
path: root/stm/stm.ml
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2017-11-27 16:50:27 +0100
committerGravatar Maxime Dénès <mail@maximedenes.fr>2017-11-27 16:50:27 +0100
commit2fcbfcfe8066bcf7ee40830bb9043b0cfd754e63 (patch)
tree0d3b52ef87e745ca91671ee37d686b0134344a53 /stm/stm.ml
parent4bf305af7e4688b96ec6f407b2a6f4e7e9d7a4a5 (diff)
parentde9b47e22811cd61316484bc8fd4ef89138ccda6 (diff)
Merge PR #6238: Fix deprecated syntax warning from vernacextend.mlp.
Diffstat (limited to 'stm/stm.ml')
0 files changed, 0 insertions, 0 deletions