tree ea0e2ae440ea582f4db831362d71575349ac3123
parent 5c021c835522d2471ff3c9ddb6dc525e0d826b0e
author Craig Scott <craig.scott@crascit.com> 1653200123 +1000
committer Craig Scott <craig.scott@crascit.com> 1653255375 +1000

ExternalProject: Remove unused property docs

BRIEF_DOCS and FULL_DOCS became optional as of edb5059216
(define_property(): Make BRIEF_DOCS and FULL_DOCS optional,
2022-01-18). Remove these options from the define_property()
calls, since they served no useful purpose. The canonical
documentation of those properties is in the RST docs at the top of
the file.