diff options
author | Juan Linietsky <reduzio@gmail.com> | 2018-11-01 12:58:14 -0300 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-11-01 12:58:14 -0300 |
commit | 1d301870ac237714a77138bf4cbc0e7b58a22baa (patch) | |
tree | 79388e39c198ceb53a905fd49f5e485e40fc5e03 /doc/tools | |
parent | 9c195b57a00f9fd3bd1ef29c5b7f8322257c01ec (diff) | |
parent | 7d82bed4f4cac8f5227d935c0496290e24eb48c8 (diff) |
Merge pull request #23169 from ibrahn/dynamic-fontlist-lifetime
Moved dynamic font list from static to lifetime controlled by main.
Diffstat (limited to 'doc/tools')
0 files changed, 0 insertions, 0 deletions