X-Git-Url: https://pintos-os.org/cgi-bin/gitweb.cgi?a=blobdiff_plain;f=doc%2Ffiles.texi;h=1323749057cf68a301ebc964edbf4b941fd796e5;hb=refs%2Fbuilds%2F20100420040526%2Fpspp;hp=2fd98927bb41e7f0bd46c95a4926d2766bfa9592;hpb=2165f59ab9eee5272b4037e45477811627cae078;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