diff options
| author | Théo Zimmermann | 2019-06-14 15:56:13 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2019-06-14 18:00:46 +0200 |
| commit | 821c1b27a9b9a849e5b29773bc775159aaa0a9d2 (patch) | |
| tree | 4d928d5032edae071afce2411d0a022658ce407d /doc/tools | |
| parent | f0d0fedd7e8ac8fbbe9f6128ea17b97792cd4dfc (diff) | |
Add a comment documenting what fontsupport.py is.
Diffstat (limited to 'doc/tools')
| -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 |