Brian Gough ad19fee667 add setting so that double flush is the default ...

can be disabled to stop flushing to track-changes

2019-11-25 13:36:25 +00:00

..

document-updater

add setting so that double flush is the default

2019-11-25 13:36:25 +00:00