Use group shortname when creating w3c.json

[dontcallmedom]

trafficstars

when https://github.com/w3c/w3c.github.io/pull/104 lands, w3c.json should accept a shortname-based version of group identification, which is easier to read and to maintain than the numeric group id; so it would be good for the repo manager to use preferentially that format.