diff options
| author | Théo Zimmermann | 2020-06-08 13:09:23 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2020-06-09 13:32:07 +0200 |
| commit | fcbae04dbe2e0777e2901cd4dff3bb5d482e3bc2 (patch) | |
| tree | 75da1a9dce4d34ba014f8e00cf6b547655c3ce52 /dev/tools/change-header | |
| parent | 4642ce1c5924cbfa93d6a8e96cf86839e614623b (diff) | |
Minor improvements to the section on basics.
Diffstat (limited to 'dev/tools/change-header')
0 files changed, 0 insertions, 0 deletions