According to the docs, the SetMIDIPlayer command can be used to set the desired MIDI player. Also:
It is permissible to include command options as well. So, for example, on Linux you might do:
SetMIDIplayer timidity -a
This works, but this does not:
SetMIDIplayer timidity -a -U
In general, one single option works, anything else is passed to player as a single, space concatenated argument.
Fix:
*** MMA/player.py~ 2012-12-29 00:07:50.000000000 +0100
--- MMA/player.py 2013-08-18 22:07:50.412426773 +0200
***************
*** 107,113 ****
cmd = [pl]
if opts:
! cmd.append(' '.join(opts))
cmd.append(file)
t=time.time()
--- 107,113 ----
cmd = [pl]
if opts:
! cmd.extend(opts)
cmd.append(file)
t=time.time()