diff --git a/collects/handin-server/scribblings/info.rkt b/collects/handin-server/scribblings/info.rkt index 76fc1f65d1..ff753f4073 100644 --- a/collects/handin-server/scribblings/info.rkt +++ b/collects/handin-server/scribblings/info.rkt @@ -1,3 +1,3 @@ #lang setup/infotab -(define scribblings '(("handin-server.scrbl" (multi-page)))) +(define scribblings '(("handin-server.scrbl" (multi-page user-doc))))