From 6295c29187b7d885a27153f6ff27d2621155c817 Mon Sep 17 00:00:00 2001
From: Ian Jackson <ijackson@chiark.greenend.org.uk>
Date: Thu, 16 May 2019 14:32:34 +0100
Subject: [PATCH] font

---
 Makefile | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Makefile b/Makefile
index cd726bf..0711b43 100644
--- a/Makefile
+++ b/Makefile
@@ -80,7 +80,7 @@ slides.ps: $(SLIDEFILES) Makefile
 	ps2pdf $< $@
 
 talk.ps: %.ps: %.txt Makefile
-	a2ps -1 -o $@.1.tmp -B $<
+	a2ps -1 -f12.5 -o $@.1.tmp -B $<
 	pstops <$@.1.tmp >$@ '0@0.94(7mm,7.5mm)'
 
 usb=/media/usb1
-- 
2.30.2