diff options
| author | Erik Martin-Dorel | 2019-03-01 19:47:41 +0100 |
|---|---|---|
| committer | Erik Martin-Dorel | 2019-04-23 12:54:43 +0200 |
| commit | c9454e2f4a083006d7145389beabcf8e4b10caa9 (patch) | |
| tree | 652d7aab00d11d8fae8ca2a6dd4fd15b61e66f81 /doc/plugin_tutorial/tuto1/src/simple_print.ml | |
| parent | f13c55b0c031b6ef92f28a3297ccfa0f7dde869d (diff) | |
[ssr] under: Add doc for {under, over} & Add entry in CHANGES.md
* For better uniformity, replace "intro-pattern" with "intro pattern"
in the ssr doc.
Diffstat (limited to 'doc/plugin_tutorial/tuto1/src/simple_print.ml')
0 files changed, 0 insertions, 0 deletions