aboutsummaryrefslogtreecommitdiff
path: root/plugins/funind
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2019-11-21 11:09:26 +0100
committerEmilio Jesus Gallego Arias2019-11-21 11:09:26 +0100
commitb680b06b31c27751a7d551d95839aea38f7fbea1 (patch)
treed02df9495e125288434cb84667df89578eb61474 /plugins/funind
parentb233d38a7a6a3e73f093c5c5ec00f1a7582e7668 (diff)
parent3a3d361e1fa3ce9a074789405f46ed4c1fc67b2f (diff)
Merge PR #11103: Grammars: unification fix/cofix between constr/vernac + cleaning
Reviewed-by: ejgallego
Diffstat (limited to 'plugins/funind')
0 files changed, 0 insertions, 0 deletions