aboutsummaryrefslogtreecommitdiff
path: root/plugins/ltac
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2018-09-26 16:07:08 +0200
committerPierre-Marie Pédrot2018-09-26 16:07:08 +0200
commit4ea1dfb16a26959843b2db6fc398556c17abd682 (patch)
treec6abdf06041752d6239700c57840cc0d3d2a0f4d /plugins/ltac
parentef231c674c11f2f7f6d87bc45f6b909aca26f0c2 (diff)
Fix votour compilation after #8102.
Diffstat (limited to 'plugins/ltac')
0 files changed, 0 insertions, 0 deletions