X-Git-Url: https://pintos-os.org/cgi-bin/gitweb.cgi?a=blobdiff_plain;f=doc%2Finvoking.texi;h=2080a3e2259b3202e54280c05537f3b848db57eb;hb=01e18746832583769419e3f59824b80229321275;hp=be89ace6104fdce4d964fb84e527330ae4de09a9;hpb=d01297fc4e5e2c48ca66c00cd78569217a5b5bc1;p=pspp

diff --git a/doc/invoking.texi b/doc/invoking.texi
index be89ace610..2080a3e225 100644
--- a/doc/invoking.texi
+++ b/doc/invoking.texi
@@ -214,17 +214,11 @@ assumed.
 @item -O orientation=@var{orientation}
 Either @code{portrait} or @code{landscape}.  Default: @code{portrait}.
 
-@item -O headers=@var{boolean}
-When enabled, headers showing the time and date, title and subtitle,
-and page number are printed at the top of each page.  Default:
-@code{on}.
-
 @item -O left-margin=@var{dimension}
 @itemx -O right-margin=@var{dimension}
 @itemx -O top-margin=@var{dimension}
 @itemx -O bottom-margin=@var{dimension}
-Sets the margins around the page.  The headers, if enabled, are not
-included in the margins; they are in addition to the margins.  See
+Sets the margins around the page.  See
 below for the allowed forms of @var{dimension} Default: @code{0.5in}.
 
 @item -O prop-font=@var{font-name}