# Preprocess the shortcuts page to get all the available shortcuts
# defined before other pages are rendered.
my $srcfile=srcfile("shortcuts.".$config{default_pageext}, 1);
# Preprocess the shortcuts page to get all the available shortcuts
# defined before other pages are rendered.
my $srcfile=srcfile("shortcuts.".$config{default_pageext}, 1);