diff options
| author | Maxime Dénès | 2018-05-28 16:29:42 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2018-05-28 16:29:42 +0200 |
| commit | 34d32da819739e795ba2b4fac96652f1fa27d969 (patch) | |
| tree | 563f7cdd2e4ac049d4396d7260071f9ef98d961f /doc/plugin_tutorial/tuto2 | |
| parent | 35b4f622a118cccf5e8dd961dd75b31c3ea9e5fd (diff) | |
Use user printer for terms instead of debug printer
Diffstat (limited to 'doc/plugin_tutorial/tuto2')
0 files changed, 0 insertions, 0 deletions