diff options
| author | Théo Zimmermann | 2017-07-29 23:40:58 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2017-07-29 23:40:58 +0200 |
| commit | a96ea9283b0eb9d4259933e673001bab5515e623 (patch) | |
| tree | 9355a8635ae6f342afa5068fff5c1272b3c0d29c /dev/include | |
| parent | 7a470793d2a8f0cecf9d552ee8a24af025a3475c (diff) | |
Drop paragraph mentioning Addendum as separate doc.
As suggested by @herbelin.
Diffstat (limited to 'dev/include')
0 files changed, 0 insertions, 0 deletions