// This is a dummy sefun file. It's
// a shortcut to avoid fixing some stuff
// before it's necessary.