diff options
| author | Erik Martin-Dorel | 2019-04-25 15:12:42 +0200 |
|---|---|---|
| committer | Erik Martin-Dorel | 2019-04-25 15:12:42 +0200 |
| commit | 05adb6e2574fa4851f6dfbcc5aa7c73254049e5c (patch) | |
| tree | 8182eb25298a4a7fba35db0ea775816ea27653cf /doc/plugin_tutorial/Makefile | |
| parent | 47f202605b4ef1795a31312b3ff2eda006fa46a6 (diff) | |
Add a typing colon in the output of the Search ssreflect vernacular
See also PR math-comp/math-comp#73
Diffstat (limited to 'doc/plugin_tutorial/Makefile')
0 files changed, 0 insertions, 0 deletions