if false {
Last monday, I bought an MP3 player for 15 €. At that price, I could'nt resist. But it cannot play the *.ogg files which I copied from my Leon Redbone CD.

Converting to *.mp3 is done by the tool ffmpeg as follows:

 ffmpeg -i song.ogg song.mp3

But the file names are much longer so I prefer a script ogg2mp3:
 }

 #! /usr/bin/tclsh
 
 proc ogg2mp3 {} {
     set rootNames {}
     foreach file [lsort [glob -nocomplain *.ogg]] {
         lappend rootNames [file rootname $file]
     }
     foreach rootName $rootNames {
         if {![file exists $rootName.mp3]} then {
             set err ""
             puts "converting $rootName ..."
             catch {exec ffmpeg -i $rootName.ogg $rootName.mp3} err
             puts $err
         }
     }
 }

 ogg2mp3