From b9841b21c21c4bee30cf1f008bd1e475f49faf88 Mon Sep 17 00:00:00 2001 From: Makarius Wenzel Date: Fri, 3 May 2002 15:13:26 +0000 Subject: fixed spelling; --- TODO | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/TODO b/TODO index f163c797..8800d46e 100644 --- a/TODO +++ b/TODO @@ -36,7 +36,7 @@ Plans for upcoming versions * Generic adjusting of pretty-printer line width (currently implemented in several instances) -* Queue manipulation improvment: allow to extend or reduce +* Queue manipulation improvement: allow to extend or reduce during processing, with fewer "Proof Process Busy" messages. * Improve process handling: disable interrupts and/or catch errors at -- cgit v1.2.3