diff options
| author |  Matej Kosik <m4tej.kosik@gmail.com> | 2015-11-06 16:58:44 +0100 |
|---|---|---|
| committer |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-12-10 09:35:17 +0100 |
| commit | a388d599ba461cf35b40c3850d593f5e9bb71d3d (patch) | |
| tree | a842271a0df1c9080e42c4cb6faac546e31bc641 /doc/refman/headers.hva | |
| parent | 56abd3ce281e3fd8f3df27597c6348d6ab033b64 (diff) | |
CLEANUP: Existing example was removed.
We have expanded the example above.
For consistency reasons, it would make sense to do the same also for this example.
However, due to the size of the terms, it is hard to typeset it nicely.
I propose to remove it.
Diffstat (limited to 'doc/refman/headers.hva')
0 files changed, 0 insertions, 0 deletions