A small gawk --profile bug

[Hermann Peifer]

Hi Arnold,

I just made a small test with the switch/case feature and saw that gawk 
--profile prints the default case twice. I guess this is a small bug.

(I was using Juergen's xgawk, which is based on gawk version 3.1.6)

Hermann


$ cat casetest.awk
{
   switch ($1) {
       case  1000:
       print "XL"
       break

       case  100:
       print "L"
       break

       case   10:
       print "M"
       break

       default:
       print "S"
   }
}

$ cat awkprof.out
       # gawk profile, created Thu Jan 21 19:45:21 2010

       # Rule(s)

       {
               switch ($1) {
               case 1000:
                       print "XL"
                       break
               case 100:
                       print "L"
                       break
               case 10:
                       print "M"
                       break
               default:
                       print "S"
               default:
                       print "S"
               }
       }