no need to suppress document sources from other sessions;
removed obsolete [document = false]: empty 'document_files' means there is no document;
Changeset
8519:796885dcfa9d
by wenzelm:
no need to suppress document sources from other sessions;<br>removed obsolete [document = false]: empty 'document_files' means there is no document;