diff options
| author | Maxime Dénès | 2019-06-06 22:05:26 +0200 |
|---|---|---|
| committer | GitHub | 2019-06-06 22:05:26 +0200 |
| commit | 26ed9cb34ea5fc84fb086644a03d016817f30a4a (patch) | |
| tree | 48b7efd13db4bbce6fb5c629c365f06d6ba3c521 /dev/tools | |
| parent | 80f3014e8360bc9c5bb21e119930bc989a8ed992 (diff) | |
Update doc/changelog/03-notations/10180-deprecate-notations.rst
Co-Authored-By: Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>
Diffstat (limited to 'dev/tools')
0 files changed, 0 insertions, 0 deletions