X-Git-Url: https://pintos-os.org/cgi-bin/gitweb.cgi?a=blobdiff_plain;f=doc%2Fdev%2Fsystem-file-format.texi;h=b0b69dd4cae54f0922bd497232811ff1bd027c1f;hb=df291f0446ae11b5a3c788a06ee73eb9ac877ca5;hp=3f82a4628e0918e1797e6c23a0670e42e0a5e8dc;hpb=c9ae1257ff1983917d2d39de53c743ae72ba16ee;p=pspp

diff --git a/doc/dev/system-file-format.texi b/doc/dev/system-file-format.texi
index 3f82a4628e..b0b69dd4ca 100644
--- a/doc/dev/system-file-format.texi
+++ b/doc/dev/system-file-format.texi
@@ -60,7 +60,8 @@ if present.
 Document record, if present.
 
 @item
-Any records not explicitly included in this list, in any order.
+Extension (type 7) records, in ascending numerical order of their
+subtypes.
 
 @item
 Dictionary termination record.