Duplicate @setfilename commands

[John Darrington]

In makeinfo/cmds.c  I see the following:

/* I don't know exactly what to do with this.  Should I allow
   someone to switch filenames in the middle of output?  Since the
   file could be partially written, this doesn't seem to make sense.
   Another option: ignore it, since they don't really want to
   switch files.  Finally, complain, or at least warn.  It doesn't
   really matter, anyway, since this doesn't get executed.  */
void
cm_setfilename (void)
{
  char *filename;
  get_rest_of_line (1, &filename);
  /* warning ("`...@%s %s' encountered and ignored", command, filename);
   */
  if (xml)
    add_word_args ("<setfilename>%s</setfilename>", filename);
  free (filename);
}


I think, at very least the warning should be uncommented. The 

    add_word_args ("<setfilename>%s</setfilename>", filename);

is wrong anyway, since it gets expanded to 
     <para>&lt;setfilename&gt;ignored&lt;/setfilename&gt;</para>

which makes for confusing reading.


J'

-- 
PGP Public key ID: 1024D/2DE827B3 
fingerprint = 8797 A26D 0854 2EAB 0285  A290 8A67 719C 2DE8 27B3
See http://pgp.mit.edu or any PGP keyserver for public key.

signature.asc
Description: Digital signature