diff options
| author | Hugo Herbelin | 2020-09-13 18:40:11 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-09-13 18:40:11 +0200 |
| commit | d7d41bee6ae195a7842c40d84162eb1e26a24533 (patch) | |
| tree | 3648797eb0d93d6204873e98df2a55103cf58d76 /dev | |
| parent | c7f1e26f3ef4862e7fc72ce76167a4c7549a2205 (diff) | |
Fixing documentation relatively to example of use of extra spaces in notations.
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions