diff options
| author | Pierre-Marie Pédrot | 2019-05-22 17:46:37 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-05-26 01:14:38 +0200 |
| commit | 1e83ae578feea41d34c3ba26a1f74c3c715620a2 (patch) | |
| tree | c67f5fd826c315191bfa666cd5e025ff396534cc /doc/plugin_tutorial | |
| parent | 51dc650f8b47a7381c19376793871817f2ef9578 (diff) | |
More precise type for Safe_typing export and inlining of private constants.
We get rid of the future wrappers, as all callers are immediately forcing
the result.
Diffstat (limited to 'doc/plugin_tutorial')
0 files changed, 0 insertions, 0 deletions