diff options
| author | Hugo Herbelin | 2020-11-05 16:17:37 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2020-11-14 22:55:47 +0100 |
| commit | 696df507b58800a7a6b52741fd4ed859aff7b1c3 (patch) | |
| tree | dff6216d09ee018319c27ca15472098f0502e039 /doc/plugin_tutorial/tuto1 | |
| parent | 0b12bb8c03b0ac7cc8aa7578a8db8ca93ecd1fd0 (diff) | |
Coqdoc: we move a newline at a better place.
This does not affect the rendering but gives better structured
html/tex files.
Diffstat (limited to 'doc/plugin_tutorial/tuto1')
0 files changed, 0 insertions, 0 deletions