diff options
Diffstat (limited to 'doc')
| -rwxr-xr-x | doc/tools/coqrst/notations/fontsupport.py | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/doc/tools/coqrst/notations/fontsupport.py b/doc/tools/coqrst/notations/fontsupport.py index a3efd97f5b..cc983565ff 100755 --- a/doc/tools/coqrst/notations/fontsupport.py +++ b/doc/tools/coqrst/notations/fontsupport.py @@ -12,6 +12,9 @@ """Transform a font to center each of its characters in square bounding boxes. See https://stackoverflow.com/questions/37377476/ for background information. + +This script is here for reference. It was used to generate the modified +font CoqNotations.ttf from UbuntuMono-B.ttf. """ from collections import Counter |