diff -r 50f22b1b136a -r 88d8d45a4cc4 doc-src/extra.sty
--- a/doc-src/extra.sty	Mon Aug 28 10:16:58 2000 +0200
+++ b/doc-src/extra.sty	Mon Aug 28 13:48:14 2000 +0200
@@ -2,10 +2,6 @@
 %
 \typeout{Document Style extra. Released 17/2/94, version of 22/8/00}
 
-\usepackage{ttbox}
-{\obeylines\gdef\ttbreak
-{\allowbreak}}
-
 %%Euro-style date: 20 September 1955
 \def\today{\number\day\space\ifcase\month\or
 January\or February\or March\or April\or May\or June\or