diff options
| author | Théo Zimmermann | 2020-05-23 13:47:08 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2020-05-27 15:38:20 +0200 |
| commit | 1f04d9e08372284ac932545292dc7a50e5226ed3 (patch) | |
| tree | a4040142fd6234685247ab750cddffcb6d6d10a9 /doc/plugin_tutorial/tuto2/src/custom.ml | |
| parent | 35e175710795974a4a38c8a7d6da6a5ccaf8de74 (diff) | |
Fix changelog for #11986.
Diffstat (limited to 'doc/plugin_tutorial/tuto2/src/custom.ml')
0 files changed, 0 insertions, 0 deletions