aboutsummaryrefslogtreecommitdiff
path: root/plugins/funind/plugin_base.dune
diff options
context:
space:
mode:
authorThéo Zimmermann2019-06-03 16:28:18 +0200
committerThéo Zimmermann2019-06-03 16:28:18 +0200
commitf051e10bbd357cd45d5b24b30abac325b0057b95 (patch)
treee7ae26c331d392fb9904fd29741c467123565618 /plugins/funind/plugin_base.dune
parent147666df9d71056e614acbab0b0b5935a085bf32 (diff)
parent573d33f49433f7b1dce3603c8138c0ded726cfc5 (diff)
Merge PR #10280: Fixed typo in CONTRIBUTING.md
Reviewed-by: Zimmi48
Diffstat (limited to 'plugins/funind/plugin_base.dune')
0 files changed, 0 insertions, 0 deletions