diff options
| author | Théo Zimmermann | 2020-05-08 12:34:14 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2020-05-08 12:34:14 +0200 |
| commit | a95ff1f5d8651a787c59acc1b5040a589725eb3b (patch) | |
| tree | 2483c3fe766f7936a31129bb8194ffa6b59ec8d9 /doc/plugin_tutorial/tuto3 | |
| parent | ca04e600e035b6822d1178cafd33848ca27446d4 (diff) | |
| parent | 665ace812f4770e8ac713d8f9c5583553c2055a8 (diff) | |
Merge PR #12281: [doc] named lemmas can be Saved too
Reviewed-by: Zimmi48
Diffstat (limited to 'doc/plugin_tutorial/tuto3')
0 files changed, 0 insertions, 0 deletions