From 821c1b27a9b9a849e5b29773bc775159aaa0a9d2 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Fri, 14 Jun 2019 15:56:13 +0200
Subject: Add a comment documenting what fontsupport.py is.

---
 doc/tools/coqrst/notations/fontsupport.py | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'doc')

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
-- 
cgit v1.2.3