diff options
| author | Théo Zimmermann | 2019-06-03 16:28:18 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2019-06-03 16:28:18 +0200 |
| commit | f051e10bbd357cd45d5b24b30abac325b0057b95 (patch) | |
| tree | e7ae26c331d392fb9904fd29741c467123565618 /plugins/firstorder/plugin_base.dune | |
| parent | 147666df9d71056e614acbab0b0b5935a085bf32 (diff) | |
| parent | 573d33f49433f7b1dce3603c8138c0ded726cfc5 (diff) | |
Merge PR #10280: Fixed typo in CONTRIBUTING.md
Reviewed-by: Zimmi48
Diffstat (limited to 'plugins/firstorder/plugin_base.dune')
0 files changed, 0 insertions, 0 deletions