diff --git a/collects/setup/setup-cmdline.rkt b/collects/setup/setup-cmdline.rkt index 0ebdfc84fe..98e677a242 100644 --- a/collects/setup/setup-cmdline.rkt +++ b/collects/setup/setup-cmdline.rkt @@ -77,7 +77,7 @@ (add-flags '((all-users #t)))] [("--mode") mode "Select a compilation mode" (add-flags `((compile-mode ,mode)))] - [("--doc-pdf") dir "Write doc PDF to