editors/with-editor: Add PDF option and change DOCS option
- Add new option PDF. If it is enabled PDF document is built and installed.
- Change DOCS option so HTML document is built and installed if it is enabled.
Description
Description
Details
Details
- Provenance
yasu Authored on Feb 20 2022, 1:23 PM - Parents
- R11:5b0b33cc004f: security/py-ropper: Update to 1.13.7
- Branches
- Unknown
- Tags