else if (state == 14 || state == 15)
{
if (ch == ')')
- state -= 14;
+ {
+ state -= 14;
+ PUT (ch);
+ ch = GET ();
+ }
else
{
PUT (ch);
/* Some relatively `normal' character. */
if (state == 0)
{
- if (IS_SYMBOL_COMPONENT (ch))
- state = 11; /* Now seeing label definition. */
+ state = 11; /* Now seeing label definition. */
}
else if (state == 1)
{
- if (IS_SYMBOL_COMPONENT (ch))
- state = 2; /* Ditto. */
+ state = 2; /* Ditto. */
}
else if (state == 9)
{