diff options
| author | Pierre-Marie Pédrot | 2017-10-27 18:42:02 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-10-27 18:56:50 +0200 |
| commit | a7c83429db05866dfc9613fc4a488d62d31386fc (patch) | |
| tree | e5f81a18dcf4ed35f089f5e9b687c87427fba119 /doc/plugin_tutorial/tuto2 | |
| parent | e0fd7c668bc284924c63a1f0a0e36fb4856c49e1 (diff) | |
Adding a notation for match goal.
Diffstat (limited to 'doc/plugin_tutorial/tuto2')
0 files changed, 0 insertions, 0 deletions