diff options
| author | Thomas Letan | 2019-07-27 13:26:17 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2020-03-28 16:53:38 +0100 |
| commit | 86d5ed1d96a93c074a070c86b1c3c81088e4cd2d (patch) | |
| tree | 6082d5fca9b134ea4f0753dd2b1dda578224f39b /tools/TimeFileMaker.py | |
| parent | 28081c1108a84050566d365bd665d05ee508ecce (diff) | |
coqdoc: Add (* begin details *) and (* end details *)
We propose to add an environment to have foldable texts with HTML
output, more precisely:
(*begin details [: An optional summary] *)
some Coq and documentation material
(* end details *)
Currently, only the HTML output is supported. We could treat this
environment in LaTeX output as appendixes to output later.
Diffstat (limited to 'tools/TimeFileMaker.py')
0 files changed, 0 insertions, 0 deletions