aboutsummaryrefslogtreecommitdiffhomepage
path: root/TODO
diff options
context:
space:
mode:
authorGravatar Makarius Wenzel <makarius@sketis.net>2002-05-03 15:13:26 +0000
committerGravatar Makarius Wenzel <makarius@sketis.net>2002-05-03 15:13:26 +0000
commitb9841b21c21c4bee30cf1f008bd1e475f49faf88 (patch)
treead399cda14514273525357ee7eb1345aba0d6c91 /TODO
parent41accc23bcf36a3b2646eb1a5f6b2db922c104fb (diff)
fixed spelling;
Diffstat (limited to 'TODO')
-rw-r--r--TODO2
1 files changed, 1 insertions, 1 deletions
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