diff options
| author | coqbot-app[bot] | 2021-02-22 11:45:00 +0000 |
|---|---|---|
| committer | GitHub | 2021-02-22 11:45:00 +0000 |
| commit | 3d1e3d41ac124a02902614317e6318d6cf7a3c38 (patch) | |
| tree | cb2a0240c94f702e8a66e8b8780e9ea5dfe55589 /doc/plugin_tutorial/tuto0 | |
| parent | 20b2dd4caea233a6516d9470619de9995bcdad96 (diff) | |
| parent | 6da4ec3e1d9e484d5cd95c116fc1c961acedf3f7 (diff) | |
Merge PR #13828: Fix doc comment in pp.mli
Reviewed-by: ejgallego
Diffstat (limited to 'doc/plugin_tutorial/tuto0')
0 files changed, 0 insertions, 0 deletions