From 072bc1110c046d367f5676fe27eba09278eb6723 Mon Sep 17 00:00:00 2001 From: Matthew Flatt Date: Thu, 2 May 2013 11:35:30 -0600 Subject: [PATCH] raco setup: add --doc-index; raco pkg: use --doc-index This combination of changes moves the decision about rebuilding "scribblings/main" and "scribblings/main/user" to `raco setup', which is in a better position to know whether documentation should be built at all. original commit: 413ca6843515dab5272d889e8a5f8df71fad9691 --- collects/setup/option-sig.rkt | 1 + 1 file changed, 1 insertion(+) diff --git a/collects/setup/option-sig.rkt b/collects/setup/option-sig.rkt index f545cca0b4..d97ad6a660 100644 --- a/collects/setup/option-sig.rkt +++ b/collects/setup/option-sig.rkt @@ -20,6 +20,7 @@ make-planet avoid-main-installation make-tidy + make-doc-index call-install call-post-install pause-on-errors