diff --git a/collects/handin-server/doc.txt b/collects/handin-server/doc.txt index 143695259f..7dd8450260 100644 --- a/collects/handin-server/doc.txt +++ b/collects/handin-server/doc.txt @@ -464,8 +464,9 @@ sub-directories: (id time-str msg-str) [|