In case of HTML export, it should be nice to add an option for the filename.The actual options are:1.) actual page number format2.) the (short) name of the page