PLAYERDRIVER_OPTION (rflex build_rflex ON)
PLAYERDRIVER_ADD_DRIVER (rflex build_rflex SOURCES rflex.cc rflex_commands.cc rflex-io.cc)
