diff options
| author | Clément Pit-Claudel | 2019-06-14 13:03:03 -0400 |
|---|---|---|
| committer | Clément Pit-Claudel | 2019-06-14 13:03:03 -0400 |
| commit | 689cfd0674fd79a21008fa7efe17774d5efaf30f (patch) | |
| tree | 43114f6486b77e1f45c6751db7ac45a9d49eb5b8 | |
| parent | a024cf9c61b57860ce3e679be4fae427996320db (diff) | |
| parent | 821c1b27a9b9a849e5b29773bc775159aaa0a9d2 (diff) | |
Merge PR #10376: Add a comment documenting what fontsupport.py is.
Reviewed-by: cpitclaudel
| -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 |