HomeIsabelle/Phabricator

discontinued redundant document_preprocessor: in the worst case, a plain-old…

Description

discontinued redundant document_preprocessor: in the worst case, a plain-old document/build script will do;

Details

Provenance
makariusAuthored on
Parents
rISABELLE015282fb3e31: clarified messages, depending on option "document_echo";
Branches
Unknown
Tags
Unknown