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.
Well, you don't want to change the format every two days for the same
basic item, but it's not a huge issue.
Richard
--
==================================================================
Richard G Heck, Jr
Professor of Philosophy
Brown University
http://frege.brown.edu/heck/
==================================================================
Get my public key from http://sks.keyserver.penguin.de
Hash: 0x1DE91F1E66FFBDEC
Learn how to sign your email using Thunderbird and GnuPG at:
http://dudu.dyn.2-h.org/nist/gpg-enigmail-howto
