diff options
| author |  Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2018-06-11 09:15:39 +0200 |
|---|---|---|
| committer | Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2018-06-17 12:48:38 +0200 |
| commit | 7f528cdb0ee42a40792d242357a239969f51cada (patch) | |
| tree | 4689d1dd9329e0c09d2ddd7c8b333a1ab3650321 /ide/idetop.ml | |
| parent | b22595da96013de18f4a2bab5e6333d75a650554 (diff) | |
Add introduction and credits to the TOC.
Move credits to its own chapter (closes #6573).
Diffstat (limited to 'ide/idetop.ml')
0 files changed, 0 insertions, 0 deletions