X-Git-Url: https://pintos-os.org/cgi-bin/gitweb.cgi?a=blobdiff_plain;f=doc%2Futilities.texi;fp=doc%2Futilities.texi;h=dcbfde14811e9f03e57dc41ac43b4f8ac7c68dae;hb=bef05451ef0f1a79d5427d5d4701b2744824c0b4;hp=c20410384ed04d38ce78838e3ed45abf76d658e7;hpb=cc2f30a26fb9dc6c0f92210c790df6c39bba038f;p=pspp

diff --git a/doc/utilities.texi b/doc/utilities.texi
index c20410384e..dcbfde1481 100644
--- a/doc/utilities.texi
+++ b/doc/utilities.texi
@@ -506,6 +506,7 @@ SET
         /CC@{A,B,C,D,E@}=@{'@var{npre},@var{pre},@var{suf},@var{nsuf}','@var{npre}.@var{pre}.@var{suf}.@var{nsuf}'@}
         /DECIMAL=@{DOT,COMMA@}
         /FORMAT=@var{fmt_spec}
+        /LEADZERO=@{ON,OFF@}
         /MDISPLAY=@{TEXT,TABLES@}
         /SMALL=@var{number}
         /WIB=@{NATIVE,MSBFIRST,LSBFIRST,VAX@}
@@ -747,6 +748,15 @@ The default @subcmd{DOT} setting causes the decimal point character to be
 Allows the default numeric input/output format to be specified.  The
 default is F8.2.  @xref{Input and Output Formats}.
 
+@item LEADZERO
+@anchor{SET LEADZERO}
+
+Controls whether numbers with magnitude less than one are displayed
+with a zero before the decimal point.  For example, with @code{SET
+LEADZERO=OFF}, which is the default, one-half is shown as 0.5, and
+with @code{SET LEADZERO=ON}, it is shown as .5.  This setting affects
+only the @code{F}, @code{COMMA}, and @code{DOT} formats.
+
 @item MDISPLAY
 @anchor{SET MDISPLAY}