;;
let add_files user files =
- let rt_dir = Helm_registry.get "matita.rt_base_dir" in
- let _repo = Helm_registry.get "matita.weblib" in
-
- let files = String.concat " "
- (List.map ((^) (rt_dir ^ "/users/" ^ user ^ "/")) files) in
-
- let errno, outlines, errlines =
- if files <> "" then
- exec_process ("svn add --non-interactive " ^ files)
- else 0,[],[]
- in
- if errno = 0 then
- "BEGIN ADD - " ^ user ^ ":\n" ^ (string_of_output outlines errlines) ^ "END ADD - " ^ user ^ "\n\n"
- else raise (SvnError (string_of_output outlines errlines))
+ if (List.length files > 0) then
+ (let rt_dir = Helm_registry.get "matita.rt_base_dir" in
+ let _repo = Helm_registry.get "matita.weblib" in
+
+ let files = String.concat " "
+ (List.map ((^) (rt_dir ^ "/users/" ^ user ^ "/")) files) in
+
+ let errno, outlines, errlines =
+ if files <> "" then
+ exec_process ("svn add --non-interactive " ^ files)
+ else 0,[],[]
+ in
+ if errno = 0 then
+ "BEGIN ADD - " ^ user ^ ":\n" ^ (string_of_output outlines errlines) ^ "END ADD - " ^ user ^ "\n\n"
+ else raise (SvnError (string_of_output outlines errlines)))
+ else ("ADD - nothing to do for " ^ user ^ "\n")
;;
(* this function should only be called by the server itself (or