diff --git a/development/tools/generate_symbols_list.py b/development/tools/generate_symbols_list.py index 02482f6d33..d640a6b729 100755 --- a/development/tools/generate_symbols_list.py +++ b/development/tools/generate_symbols_list.py @@ -12,11 +12,15 @@ import sys,string,re,os,os.path import io def get_code(code, font): - if font != "dontknowwhichfontusesthisstrangeencoding": + # computer modern fonts use a strange encoding + cmfonts = ["cmex", "cmr", "cmm", "cmsy"] + if font not in cmfonts: return code if code < 10: return code+161 - elif code < 32: + if code < 11: + return code+162 + elif code <= 32: return code+163 else: return code