X-Git-Url: https://pintos-os.org/cgi-bin/gitweb.cgi?a=blobdiff_plain;f=doc%2Ffiles.texi;h=1323749057cf68a301ebc964edbf4b941fd796e5;hb=693707ea5cbef6da4a83010ea734ef8568b983d3;hp=2fd98927bb41e7f0bd46c95a4926d2766bfa9592;hpb=a1efcf97ca2f75f4be6a0389ff2372c03ed2d4e1;p=pspp

diff --git a/doc/files.texi b/doc/files.texi
index 2fd98927bb..1323749057 100644
--- a/doc/files.texi
+++ b/doc/files.texi
@@ -800,4 +800,3 @@ the data is read by a procedure or procedure-like command.
 @end itemize
 
 @xref{SAVE}, for more information.
-@setfilename ignored