diff --git a/collects/setup/option-sig.ss b/collects/setup/option-sig.ss index 517d218662..cd577e538e 100644 --- a/collects/setup/option-sig.ss +++ b/collects/setup/option-sig.ss @@ -14,9 +14,12 @@ make-so make-info-domain make-launchers + make-docs call-install + call-post-install pause-on-errors force-unpacks + doc-pdf-dest specific-collections specific-planet-dirs archives