aboutsummaryrefslogtreecommitdiff
path: root/plugins/funind/plugin_base.dune
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2020-04-03 10:56:25 -0400
committerEmilio Jesus Gallego Arias2020-04-03 10:56:25 -0400
commit8a3255bc99691c7c0f9b386e63b7947169f902b7 (patch)
treeebffb272641a2b63a6217692a6c64fc1fa83e3ad /plugins/funind/plugin_base.dune
parenta37814ae4df4a97c0b5bdbef68d72e52412e5467 (diff)
parent7540acc5f0ced610d9fc10560d75990be3c9cd9a (diff)
Merge PR #11895: Remove Chapter command.
Reviewed-by: ejgallego
Diffstat (limited to 'plugins/funind/plugin_base.dune')
0 files changed, 0 insertions, 0 deletions