diff --git a/collects/handin-server/main.ss b/collects/handin-server/main.ss index 1365816a05..8d08230fc1 100644 --- a/collects/handin-server/main.ss +++ b/collects/handin-server/main.ss @@ -94,6 +94,7 @@ (copy-directory/files dir/f f)] [(or (<= (file-or-directory-modify-seconds f) (file-or-directory-modify-seconds dir/f)) + ;; just in case, check the size too: (and (file-exists? f) (file-exists? dir/f) (not (= (file-size f) (file-size dir/f))))) ;; f is newer in dir than in the working directory