diff options
| author | Pierre-Marie Pédrot | 2017-10-30 18:16:18 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-10-30 18:16:18 +0100 |
| commit | de7483beb78e5bd81dc6449ba201fb9dfc490ba8 (patch) | |
| tree | 607bccab68053410b42f4d767cf7a5dd6aae61f6 /doc/plugin_tutorial | |
| parent | 2f95db622428cf58968e8d13f2230fe51c31e97f (diff) | |
Add a macro for the now tactic
Diffstat (limited to 'doc/plugin_tutorial')
0 files changed, 0 insertions, 0 deletions