prefs); print_prefs_display($prefs); } echo "

\n"; page_tail(); ?>