Re: strange looking HTML menus

[Eli Zaretskii]

> From: address@hidden (Karl Berry)
> Date: Mon, 18 Mar 2002 12:16:22 -0500
> 
>     Can someone please tell me why we have the final `:'?  
> 
> Just came out that way.

The code seems to do this on purpose:

      if (looking_at ("::"))
        discard_until (":");
      else
        { /* discard the node name */
          get_until_in_line (0, ".", &string);
          free (string);
        }
      input_text_offset++;      /* discard the second colon or the period */
      add_word (": ");

See that last add_word?

I don't remember why is it done so, but I'd suggest to be
extra-careful with changing that, especially in a bug-fix release.