diff options
| author | Hugo Herbelin | 2019-12-09 17:10:26 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2020-02-23 08:26:46 +0100 |
| commit | 8031bc3963e2c25e04775f5445cc11ad8b5d83e1 (patch) | |
| tree | c28139163a3e8cf4b66f3a71bd7bff3fe4aa1efa /dev | |
| parent | 12d2e91a9018d2189b041249c440d483c14b5575 (diff) | |
Apply and generalize suggestions from Théo.
Co-Authored-By: Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions