aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev/top_printers.mli
diff options
context:
space:
mode:
authorGravatar Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>2018-06-11 09:15:39 +0200
committerGravatar Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>2018-06-17 12:48:38 +0200
commit7f528cdb0ee42a40792d242357a239969f51cada (patch)
tree4689d1dd9329e0c09d2ddd7c8b333a1ab3650321 /dev/top_printers.mli
parentb22595da96013de18f4a2bab5e6333d75a650554 (diff)
Add introduction and credits to the TOC.
Move credits to its own chapter (closes #6573).
Diffstat (limited to 'dev/top_printers.mli')
0 files changed, 0 insertions, 0 deletions