diff options
| author | Yves Bertot | 2018-05-30 15:06:24 +0200 |
|---|---|---|
| committer | GitHub | 2018-05-30 15:06:24 +0200 |
| commit | 470f48c60124aaad7d5825959630453108c99f1b (patch) | |
| tree | 563f7cdd2e4ac049d4396d7260071f9ef98d961f /doc/plugin_tutorial/README.md | |
| parent | 35b4f622a118cccf5e8dd961dd75b31c3ea9e5fd (diff) | |
| parent | 34d32da819739e795ba2b4fac96652f1fa27d969 (diff) | |
Merge pull request #6 from maximedenes/fix-printer
Use user printer for terms instead of debug printer
Diffstat (limited to 'doc/plugin_tutorial/README.md')
0 files changed, 0 insertions, 0 deletions