>> there is additional patch in my stack which improves detection of changed >> settings in case 'use hyperref' is disabled and which get rid off saving >> store_option flag. this would however again change fileformat and its >> not clear to me, whether is good idea to proceed this way. > > I don't know why this would be needed. From my point of view the current > implementation is OK.
its rather minor issue - when the user temporarily switch off hyperref support, his settings(eg checkboxes) will be saved only if he filled some text edit field. pavel
