X-Git-Url: https://pintos-os.org/cgi-bin/gitweb.cgi?a=blobdiff_plain;f=doc%2Futilities.texi;h=95cfa25dd89d472c615461f51f4eabb1aa0299dc;hb=1288f8123ea04686150b79b9e6a5d5d78c420353;hp=d825b9abc4a5e0e6a676ecd2c258bbb5f7d06e77;hpb=a1efcf97ca2f75f4be6a0389ff2372c03ed2d4e1;p=pspp-builds.git

diff --git a/doc/utilities.texi b/doc/utilities.texi
index d825b9ab..95cfa25d 100644
--- a/doc/utilities.texi
+++ b/doc/utilities.texi
@@ -787,4 +787,3 @@ on the output device.
 Specify a title as a string in quotes.  The alternate syntax that did
 not require quotes is now obsolete.  If it is used then the title is
 converted to all uppercase.
-@setfilename ignored