/* srmmu.c */
  extern char *srmmu_name;
  
  extern void (*poke_srmmu)(void);