All: We don't want to hard-code something like ogg123 as the handler or even as a possible handler for the sound files if we plan to ever handle any other extension than .oga or .ogg because ogg123 only handles ogg.

We don't even want it to be an option because if we play something with some other extension it won't work at best and it might hang (zombie) or cause a horrible clicking white-noise racket by playing the wrong format.

This "racket" does happen with other players trying to play mp3s, not sure about ogg123.

const char *players[] = { "play", "gst123", "ogg123" };