/* Machine-generated C-file- do not edit ! */
char __diskfontname[]="diskfont.library";