diff options
| author | Emilio Jesus Gallego Arias | 2019-12-05 23:44:58 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-01-03 12:00:04 +0100 |
| commit | aad86c49b55bbdaa916c10b84272bec5a2b6a678 (patch) | |
| tree | 4e3fecb85f05af79f1642a5df9a26eb6c5f00367 /dev | |
| parent | 524d0be2e3dd70090dbd9f98a065390610e96ef5 (diff) | |
[tools] Remove support for python2
Closes #10491
We re-add the header in doc/tools/coqrst/notations/fontsupport.py
which was removed by accident in 1a9c769ed363ee2f2784e7252af72e6c1e2fbcc6
The fontsupport script itself has been kept for reference, however it
is not involved by any build target as of today.
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions