X-Git-Url: https://pintos-os.org/cgi-bin/gitweb.cgi?a=blobdiff_plain;f=doc%2Fdata-file-format.texi;h=2186b6d411089552ca91d281d9f9388df43854a1;hb=a89f1b18969c1c9603fc67aee3055585af9d167c;hp=5c900244f50daa9ae05ca191f9f038feb18d9508;hpb=3e393e4601620af7583ca2b748def2ed08b468ec;p=pspp

diff --git a/doc/data-file-format.texi b/doc/data-file-format.texi
index 5c900244f5..2186b6d411 100644
--- a/doc/data-file-format.texi
+++ b/doc/data-file-format.texi
@@ -135,7 +135,7 @@ format and using 24-hour time.  If the time is not available then this
 field is arbitrarily set to @samp{00:00:00}.
 
 @item char file_label[64];
-Set the the file label declared by the user, if any (@pxref{FILE LABEL}).
+Set the file label declared by the user, if any (@pxref{FILE LABEL}).
 Padded on the right with spaces.
 
 @item char padding[3];