diff options
| author | Théo Zimmermann | 2019-10-06 13:18:10 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2019-10-06 13:22:59 +0200 |
| commit | 817b32d7a01dea3988f25e1130ffbb2d091837b3 (patch) | |
| tree | 71964e5419d53abd1c1b2d0f612ce701b7b3644d /dev | |
| parent | 97a2047d32aa1dc8689ff65eff5f82a6efa74656 (diff) | |
Fix #10831: minor issues in documentation of Function.
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions