diff options
| author |  Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2015-07-31 17:28:40 +0200 |
|---|---|---|
| committer | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2015-07-31 17:28:40 +0200 |
| commit | 71e0a34f89d03787003df1a30bb793bd71ebb775 (patch) | |
| tree | 4357cdaa3b229a8780eb07ff798aa966236686bd /toplevel | |
| parent | 947206269dc31bb6b919fce935e1748bc440d960 (diff) | |
Fix typos in the Extraction part of the reference manual.
In particular, fix the name of all the user contributions.
Diffstat (limited to 'toplevel')
0 files changed, 0 insertions, 0 deletions