diff options
| author | Sebastian Kuzminsky <seb@highlab.com> | 2016-02-28 22:24:09 -0700 |
|---|---|---|
| committer | Sebastian Kuzminsky <seb@highlab.com> | 2016-03-28 21:55:19 -0600 |
| commit | 1d78ebaf9b518d96230ae19c958aedf8873a31f6 (patch) | |
| tree | 27078a0d3589b72ec4cb75d9df129db54a82dbfb /debian/patches/series | |
| parent | a9737066a11cbd137c5d370cc66e1c21b5d107f4 (diff) | |
switch to a free font for the manual
This switches the manual's font from luximono (which is non-free, and
not available in Debian) to libertine.
Diffstat (limited to 'debian/patches/series')
| -rw-r--r-- | debian/patches/series | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/debian/patches/series b/debian/patches/series index 0c249a07..964a4a7f 100644 --- a/debian/patches/series +++ b/debian/patches/series @@ -3,3 +3,4 @@ 03_notruntests.patch 05_abc_executable.patch spelling-fixes.patch +switch-to-free-font.patch |