X-Git-Url: https://pintos-os.org/cgi-bin/gitweb.cgi?a=blobdiff_plain;f=doc%2Fcommand-index.texi;h=d26f9074704f2ac3024871f07403aae4e80e069f;hb=a554ee5cd3f34f39bd202f6a40a79256b537c40d;hp=c53b1db6e86af0c1ef9f593b1d37480105a77ef7;hpb=00feff7775f55b3292d1f9461a79dde54b9eb2ba;p=pspp

diff --git a/doc/command-index.texi b/doc/command-index.texi
index c53b1db6e8..d26f907470 100644
--- a/doc/command-index.texi
+++ b/doc/command-index.texi
@@ -1,4 +1,3 @@
 @node Command Index
 @chapter Command Index
 @printindex vr
-@setfilename ignored