diff options
| author | Enrico Tassi | 2019-04-26 11:28:27 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2019-04-26 11:28:27 +0200 |
| commit | e518ed1ff4121cd5e5be0e970c88e19bf29552c2 (patch) | |
| tree | 4149c55216f17cf4e42682bf0e2f61b1b33cccab /doc/plugin_tutorial/tuto1/Makefile | |
| parent | 12e5d3cdef8b954fc3a7cdf1dfebc388bd546c3a (diff) | |
| parent | 05adb6e2574fa4851f6dfbcc5aa7c73254049e5c (diff) | |
Merge PR #10001: Add a typing colon in the output of the Search ssreflect vernacular
Reviewed-by: gares
Diffstat (limited to 'doc/plugin_tutorial/tuto1/Makefile')
0 files changed, 0 insertions, 0 deletions